Fix duplicate variable issue in sygus-qe-preproc (#4013)

diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index a0e25b7567c4e1146e4aa650c5a157969cb3e79d..50831fdac8acd74fbc363f1b520b31d5469c4a13 100644 (file)
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -346,7 +346,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
       d_conjuncts[2].push_back(cr);
       std::unordered_set<Node, NodeHashFunction> fvs;
       expr::getFreeVariables(cr, fvs);
-      d_all_vars.insert(d_all_vars.end(), fvs.begin(), fvs.end());
+      d_all_vars.insert(fvs.begin(), fvs.end());
       if (singleInvocation)
       {
         // replace with single invocation formulation

diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h
index 0a4af3185b416527aae3dd5897ed71dce0abce86..cdc56d1f0955f77ee36db1d8a0b92ea1b036a2f9 100644 (file)
--- a/src/theory/quantifiers/single_inv_partition.h
+++ b/src/theory/quantifiers/single_inv_partition.h
@@ -201,7 +201,7 @@ class SingleInvocationPartition
   std::vector<Node> d_si_vars;
 
   /** every free variable of conjuncts[2] */
-  std::vector<Node> d_all_vars;
+  std::unordered_set<Node, NodeHashFunction> d_all_vars;
   /** map from functions to first-order variables that anti-skolemized them */
   std::map<Node, Node> d_func_fo_var;
   /** map from first-order variables to the function it anti-skolemized */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 15728ec1d019fd1b6c6226d1681641aa7a2040c6..83d9ac48cb538b48884e6ebe01703a3f2f7dc39d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1855,6 +1855,7 @@ set(regress_1_tests
   regress1/sygus/issue3839-cond-rewrite.smt2
   regress1/sygus/issue3944-div-rewrite.smt2
   regress1/sygus/issue3947-agg-miniscope.smt2
+  regress1/sygus/issue4009-qep.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/issue4009-qep.smt2 b/test/regress/regress1/sygus/issue4009-qep.smt2
new file mode 100644 (file)
index 0000000..6f17a0c
--- /dev/null
+++ b/test/regress/regress1/sygus/issue4009-qep.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inference --sygus-qe-preproc
+(set-logic ALL)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (forall ((c Real)) (and (xor (> c a) (= b 0)) (distinct (+ a b) 0))))
+(check-sat)