diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-05-19 18:05:07 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-19 21:05:07 +0000 |
| commit | 1c0a94f3797c0746c760009975012cfd0a247583 (patch) | |
| tree | 9f306a9fc45c978fafef2f662c4f21a78016e84f /test/regress/regress1 | |
| parent | 467a94cde962d90d3970c4378fc5f2b8a2476352 (diff) | |
Adding regressions that failed on old unsat cores (#6574)
We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/cores/issue5604.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress1/cores/issue5604.smt2 b/test/regress/regress1/cores/issue5604.smt2 new file mode 100644 index 000000000..e41335a4a --- /dev/null +++ b/test/regress/regress1/cores/issue5604.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: unsat +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(assert (xor (str.prefixof (str.replace "B" (str.substr a 0 (str.len b)) "") b) (str.prefixof "B" b))) +(assert (= a (str.++ b c))) +(check-sat) |