Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This would crash before: (declare-fun x () (_ BitVec 4)) (assert (not (bvule x #x1))) (apply elim-uncnstr2) That's because the index_set iterator was querying qtail to compute the end of the iteration But the problem is that elim-uncnstr2 may add new fmls to the goal, as in this case. The bvule is replaced with an 'or', but since it's negated, it turns into 2 goals Solve the issue by freezing the qtail for the iteration loop. This is the right behavior for elim-uncnstr2, as it can't rewrite exprs that haven't been analyzed before @NikolajBjorner please check if this the right behavior for the other simplifiers. Thank you
- Loading branch information
a302c2f
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
doesn't work with tactics: if you add "false" to a goal it truncates.