java-backend bugfix: ConjunctiveFormula.simplify(): properly restore the constraint on all execution paths.
@@ -386,6 +386,7 @@ public class ConjunctiveFormula extends Term implements CollectionInternalRepres
PersistentUniqueList<Equality> equalities = this.equalities;
PersistentUniqueList<DisjunctiveFormula> disjunctions = this.disjunctions;
+ try {
boolean change;
do {
change = false;
@@ -505,8 +506,10 @@ public class ConjunctiveFormula extends Term implements CollectionInternalRepres
equalities = pendingEqualities;
} while (change);
- context.setTopConstraint(originalTopConstraint);
return ConjunctiveFormula.of(substitution, equalities, disjunctions, global);
+ } finally {
+ context.setTopConstraint(originalTopConstraint);
+ }
}
private ConjunctiveFormula falsify(
