diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-24 12:41:34 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-24 12:41:34 -0500 |
| commit | cecaa8b28477d6bef96ece4976d5383e9b3cd4d1 (patch) | |
| tree | f6d3fe2b2af3485345db3170b8e409be736809ef | |
| parent | ecafdf215735ad9d8257dc44064f2479502d348b (diff) | |
| parent | be607a9d420f79fa3e6a1f2c9b8c0e1b49cd34ee (diff) | |
Merge branch 'master' into fixExtraVersionfixExtraVersion
| -rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 10 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/unconstrained/issue4644.smt2 | 9 |
3 files changed, 20 insertions, 0 deletions
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index e20403d2a..7d1f66d65 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -75,6 +75,16 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) { d_unconstrained.erase(current); } + else + { + // Also erase the children from the visited-once set when we visit a + // node a second time, otherwise variables in this node are not + // erased from the set of unconstrained variables. + for (TNode childNode : current) + { + toVisit.push_back(unc_preprocess_stack_element(childNode, current)); + } + } } ++find->second; continue; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index bb0f311d1..7863c5ec0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1178,6 +1178,7 @@ set(regress_0_tests regress0/unconstrained/bvult5.smt2 regress0/unconstrained/geq.smt2 regress0/unconstrained/gt.smt2 + regress0/unconstrained/issue4644.smt2 regress0/unconstrained/ite.smt2 regress0/unconstrained/leq.smt2 regress0/unconstrained/lt.smt2 diff --git a/test/regress/regress0/unconstrained/issue4644.smt2 b/test/regress/regress0/unconstrained/issue4644.smt2 new file mode 100644 index 000000000..aeb2bfc84 --- /dev/null +++ b/test/regress/regress0/unconstrained/issue4644.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --unconstrained-simp +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (distinct a c)) +(assert (= a b (= b c))) +(set-info :status sat) +(check-sat) |