diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 4 | ||||
| -rw-r--r-- | test/regress/regress0/strings/code-sat-neg-one.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/strings/strings-leq-trans-unsat.smt2 | 14 | ||||
| -rw-r--r-- | test/regress/regress1/strings/strings-lt-len5.smt2 | 9 | ||||
| -rw-r--r-- | test/regress/regress1/strings/strings-lt-simple.smt2 | 8 |
5 files changed, 42 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 8584eeca9..cf702ed7c 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -776,6 +776,7 @@ REG0_TESTS = \ regress0/strings/bug002.smt2 \ regress0/strings/bug612.smt2 \ regress0/strings/bug613.smt2 \ + regress0/strings/code-sat-neg-one.smt2 \ regress0/strings/escchar.smt2 \ regress0/strings/escchar_25.smt2 \ regress0/strings/idof-rewrites.smt2 \ @@ -1452,6 +1453,9 @@ REG1_TESTS = \ regress1/strings/str007.smt2 \ regress1/strings/string-unsound-sem.smt2 \ regress1/strings/strings-index-empty.smt2 \ + regress1/strings/strings-leq-trans-unsat.smt2 \ + regress1/strings/strings-lt-len5.smt2 \ + regress1/strings/strings-lt-simple.smt2 \ regress1/strings/strip-endpt-sound.smt2 \ regress1/strings/str-code-sat.smt2 \ regress1/strings/str-code-unsat.smt2 \ diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2 new file mode 100644 index 000000000..c69276a4f --- /dev/null +++ b/test/regress/regress0/strings/code-sat-neg-one.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(assert (not (= x y))) +(assert (= (str.code x) (str.code y))) +(check-sat) diff --git a/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 new file mode 100644 index 000000000..de3946ef0 --- /dev/null +++ b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) +(assert (str.<= x y)) +(assert (str.<= y w)) +(declare-fun xp () String) +(assert (= x (str.++ "G" xp))) +(assert (= w "E")) +(check-sat) diff --git a/test/regress/regress1/strings/strings-lt-len5.smt2 b/test/regress/regress1/strings/strings-lt-len5.smt2 new file mode 100644 index 000000000..aeabfdf75 --- /dev/null +++ b/test/regress/regress1/strings/strings-lt-len5.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun y () String) +(assert (> (str.len y) 5)) +(assert (str.< "ACAAB" y)) +(assert (str.< y "ACAAD")) +(check-sat) diff --git a/test/regress/regress1/strings/strings-lt-simple.smt2 b/test/regress/regress1/strings/strings-lt-simple.smt2 new file mode 100644 index 000000000..e077cf1f7 --- /dev/null +++ b/test/regress/regress1/strings/strings-lt-simple.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(declare-fun y () String) +(assert (str.< "AC" y)) +(assert (str.< y "AF")) +(check-sat) |