diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-05 16:35:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-05 14:35:44 -0700 |
commit | 21376f1b756a237004adb9ba11c10566685a9605 (patch) | |
tree | ae37a6f8abb2d1b60938b13385ced707f576904d /src/preprocessing | |
parent | d66146480789917cb7d5c49dc9b603f40d6851fc (diff) |
Always introduce fresh variable for unconstrained APPLY_UF (#4472)
Fixes an unsoundness in unconstrained simplification, fixes #4469.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 11 |
1 files changed, 7 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); } |