-
Alexandre Duret-Lutz authored
* src/ltlvisit/length.hh (length_boolone): New function. * src/ltlvisit/length.cc (length_boolone): Implement it using... (length_boolone_visitor): ... this new visitor. * src/ltltest/randltl.cc: Use length_boolone() to check the result of the random generator, and ignore any formula larger (in length()) than opt_f. This fix a bug where the random formula generator would sometime produce formula larger than requested, because of the trivial rewriting of {f}[]->e as e|!f. * src/ltltest/length.cc: Add option -b to call length_boolone(). * src/ltltest/length.test: Test length_boolone().
ed0dd0b4