diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-27 20:28:20 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-27 20:28:20 -0700 |
| commit | 972dcfafe5eeb10b7b45892d1291000e73746c76 (patch) | |
| tree | 114c1210c913a7d6dd4ece1bcca700d0f1ac1f53 /test/regress | |
| parent | a1624b7f5b7809329845f4a31e7b6a0e86ebc9d3 (diff) | |
`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)
Fixes #5508. `STRINGS_CTN_DECOMPOSE` could be triggered multiple times
by the same term, which resulted in an assertion failure. This commit
returns immediately after the first conflict to avoid the assertion
failure.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/issue5508-multiple-conflicts.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e10b89c79..7de2d9789 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1132,6 +1132,7 @@ set(regress_0_tests regress0/strings/issue5090.smt2 regress0/strings/issue5384-double-conflict.smt2 regress0/strings/issue5428-re-diff-assoc.smt2 + regress0/strings/issue5508-multiple-conflicts.smt2 regress0/strings/issue5542-strings-seq-mix.smt2 regress0/strings/issue5608-eager-pp.smt2 regress0/strings/issue5666-orig-unit-deq.smt2 diff --git a/test/regress/regress0/strings/issue5508-multiple-conflicts.smt2 b/test/regress/regress0/strings/issue5508-multiple-conflicts.smt2 new file mode 100644 index 000000000..1d7d208c9 --- /dev/null +++ b/test/regress/regress0/strings/issue5508-multiple-conflicts.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(declare-fun i2 () Int) +(declare-fun str10 () String) +(declare-fun str19 () String) +(declare-fun i19 () Int) +(assert (str.contains (str.from_int i2) (str.++ str19 "uKykCsFtVM" (str.from_int i19) "hORknmKIFtylbjBJVLsMNyAUKzpayeBQPHqN" str10))) +(set-info :status unsat) +(check-sat) |