diff options
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 8 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue4083-var-shadow.smt2 | 8 |
3 files changed, 14 insertions, 3 deletions
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) |