From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Mar 2020 22:29:41 +0000 (-0500)
Subject: Fix variable shadowing issue in sygus-inference (#4121)
X-Git-Tag: cvc5-1.0.0~3462
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a0cee14c38cac0f87772c192ef387dcd36b6977;p=cvc5.git

Fix variable shadowing issue in sygus-inference (#4121)

This makes the sygus-inference preprocessing pass avoid variable shadowing, which technically could happen by forcing unexpected options.

Fixes #4083.
---

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 41bb226a3..776e738d3 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -154,16 +154,18 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
         TypeNode tnv = v.getType();
         unsigned vnum = type_count[tnv];
         type_count[tnv]++;
+        vars.push_back(v);
         if (vnum < qtvars[tnv].size())
         {
-          vars.push_back(v);
           subs.push_back(qtvars[tnv][vnum]);
         }
         else
         {
           Assert(vnum == qtvars[tnv].size());
-          qtvars[tnv].push_back(v);
-          qvars.push_back(v);
+          Node bv = nm->mkBoundVar(tnv);
+          qtvars[tnv].push_back(bv);
+          qvars.push_back(bv);
+          subs.push_back(bv);
         }
       }
       pas = pas[1];
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 50ef63780..a8ec4a665 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1867,6 +1867,7 @@ set(regress_1_tests
   regress1/sygus/issue3995-fmf-var-op.smt2
   regress1/sygus/issue4009-qep.smt2
   regress1/sygus/issue4025-no-rlv-cond.smt2
+  regress1/sygus/issue4083-var-shadow.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
diff --git a/test/regress/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
new file mode 100644
index 000000000..bb9434860
--- /dev/null
+++ b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :miniscope-quant true)
+(set-option :sygus-inference true)
+(set-option :var-ineq-elim-quant false)
+(set-info :status unsat)
+(declare-fun b ( Int ) Bool)
+(assert (forall (( c Int ) ( d Int )) (and (> d 3 ) (xor (>= c d) (b c)))))  
+(check-sat)