Bug in generator creation
Issue #588
resolved
For the attached file, if longestbranch is set high enough (+30), propagation derives a bdd for which the generator is wrong about half of the time, resulting in unsat. The easiest to see is to call, in applypropagationtostructure, the line that prints the derived symbols multiple times.
The problem seems that be that one of the checks for a domain element to be in the inverse una table of pos is just plainly and incorrectly dropped.
Comments (4)
-
-
reporter
- changed title to Bug in generator creation
- marked as critical
- edited description
- attached command.idp
-
reporter
- changed status to resolved
Fixes
#588:: inverseUNAgenerator ignored the IN part of its pattern.→ <<cset 661c51b3af75>>
-
Merged in fix_inverseUNA_588 (pull request #152)
Fixes
#588:: inverseUNAgenerator ignored the IN part of its pattern.→ <<cset 67d43317ba5e>>
- Log in to comment
Tested it on the current master, but I always get 5 solutions.