From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 5 May 2020 21:35:44 +0000 (-0500)
Subject: Always introduce fresh variable for unconstrained APPLY_UF (#4472)
X-Git-Tag: cvc5-1.0.0~3322
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21376f1b756a237004adb9ba11c10566685a9605;p=cvc5.git

Always introduce fresh variable for unconstrained APPLY_UF (#4472)

Fixes an unsoundness in unconstrained simplification, fixes #4469.
---

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)