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/regress0 | |
| 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/regress0')
| -rw-r--r-- | test/regress/regress0/strings/issue5508-multiple-conflicts.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
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) |