diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-23 16:57:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-23 21:57:13 +0000 |
| commit | a9ac3972bd3d0f0328e957bc04d8c0ef12811a51 (patch) | |
| tree | 511dbc95203898fcfafa646db23a20ac2045f215 /test/regress | |
| parent | 982b585a1b766a933055d7328579cdb482504fe4 (diff) | |
Purify substitutions in strings proof reconstruction (#7035)
This fixes an issue in strings proof reconstruction where sequential substitutions are used over possibly non-atomic terms like (str.replace x a b) and x simultaneously.
This leads to cases where we failed to reconstruct proofs, since a substitution x -> c, (str.replace x a b) -> d may unintentionally generate the term (str.replace c a b), after which the second substitution fails to apply.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/delta-trust-subs.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 55649c2f0..ce047c877 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1149,6 +1149,7 @@ set(regress_0_tests regress0/strings/code-perf.smt2 regress0/strings/code-sat-neg-one.smt2 regress0/strings/complement-simple.smt2 + regress0/strings/delta-trust-subs.smt2 regress0/strings/escchar_25.smt2 regress0/strings/escchar.smt2 regress0/strings/from_code.smt2 diff --git a/test/regress/regress0/strings/delta-trust-subs.smt2 b/test/regress/regress0/strings/delta-trust-subs.smt2 new file mode 100644 index 000000000..eb3c90374 --- /dev/null +++ b/test/regress/regress0/strings/delta-trust-subs.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () String) +(assert (= (str.++ a "0" (str.++ a a) "A") (str.++ "0" (str.from_code (str.len a)) (str.replace "A" (str.++ a "A") a)))) +(check-sat) |