diff options
| -rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 11 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/issue4469-unc-no-reuse-var.smt2 | 7 |
3 files changed, 15 insertions, 4 deletions
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 8a2c58b99..7cf6a79bd 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -577,10 +577,9 @@ void UnconstrainedSimplifier::processUnconstrained() { currentSub = current; } - if (parent.getType() != current.getType()) - { - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - } + // always introduce a new variable; it is unsound to try to reuse + // currentSub as the variable, see issue #4469. + currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; } else @@ -779,6 +778,10 @@ void UnconstrainedSimplifier::processUnconstrained() } if (!currentSub.isNull()) { + Trace("unc-simp") + << "UnconstrainedSimplifier::processUnconstrained: introduce " + << currentSub << " for " << current << ", parent " << parent + << std::endl; Assert(currentSub.isVar()); d_substitutions.addSubstitution(current, currentSub, false); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 97a521028..b8304f722 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -552,6 +552,7 @@ set(regress_0_tests regress0/issue1063-overloading-dt-sel.smt2 regress0/issue2832-qualId.smt2 regress0/issue4010-sort-inf-var.smt2 + regress0/issue4469-unc-no-reuse-var.smt2 regress0/ite.cvc regress0/ite2.smt2 regress0/ite3.smt2 diff --git a/test/regress/regress0/issue4469-unc-no-reuse-var.smt2 b/test/regress/regress0/issue4469-unc-no-reuse-var.smt2 new file mode 100644 index 000000000..3bc79578f --- /dev/null +++ b/test/regress/regress0/issue4469-unc-no-reuse-var.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --unconstrained-simp --no-check-models +; EXPECT: sat +(set-logic QF_AUFBVLIA) +(declare-fun a () Int) +(declare-fun b (Int) Int) +(assert (distinct (b a) (b (b a)))) +(check-sat) |