diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-26 00:46:17 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-26 00:46:17 +0100 |
| commit | 1c7ed68156cb3cf19ef036cbbfff18bcc4e45c36 (patch) | |
| tree | e7e5a8daf5a07174a3c7180e437d711ea243bba1 /test/regress | |
| parent | ac30758787c01f532774501a06b5cbdc713074dd (diff) | |
Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/preprocess/issue5943-non-clausal-simp.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b08777a51..1a43b0335 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -746,6 +746,7 @@ set(regress_0_tests regress0/precedence/xor-or.cvc regress0/preprocess/circuit-prop.smt2 regress0/preprocess/issue5729-rewritten-assertions.smt2 + regress0/preprocess/issue5943-non-clausal-simp.smt2 regress0/preprocess/preprocess_00.cvc regress0/preprocess/preprocess_01.cvc regress0/preprocess/preprocess_02.cvc diff --git a/test/regress/regress0/preprocess/issue5943-non-clausal-simp.smt2 b/test/regress/regress0/preprocess/issue5943-non-clausal-simp.smt2 new file mode 100644 index 000000000..f3abedcdf --- /dev/null +++ b/test/regress/regress0/preprocess/issue5943-non-clausal-simp.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic QF_SLIA) +(declare-fun s () String) +(assert (and (and (= (str.len (str.at s 3)) 4) (not (not (= (ite (not (= (ite (not (= (str.at (str.at s 3) +(ite (not (not (= (ite (<= (str.len (str.at s 1)) 3) 1 0) 0))) 1 0)) (str.at s 5))) 1 0) 0)) 1 0) 0)))) (not (not (= (str.len s) 3))))) +(check-sat) |