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 41bb226a307cb4321be5093c2ff04e721d777398..776e738d33bf5a2b93339b4fffbd0e296aa734c5 100644 (file)
--- 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 50ef63780e4ebd670718702dc951205c13940a90..a8ec4a6650eb883729dd1215e9a437ba898bb52a 100644 (file)
--- 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 (file)
index 0000000..bb94348
--- /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)