diff options
Diffstat (limited to 'test/regress/regress0/strings/strip-endpt-sound.smt2')
-rw-r--r-- | test/regress/regress0/strings/strip-endpt-sound.smt2 | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/test/regress/regress0/strings/strip-endpt-sound.smt2 b/test/regress/regress0/strings/strip-endpt-sound.smt2 deleted file mode 100644 index 0c1dd123c..000000000 --- a/test/regress/regress0/strings/strip-endpt-sound.smt2 +++ /dev/null @@ -1,29 +0,0 @@ -; COMMAND-LINE: --strings-exp -; EXPECT: sat -(set-logic QF_S) -(declare-fun x () String) -(declare-fun y () String) - -(assert (str.contains "c(ab)" (str.++ x ")"))) -(assert (str.contains "c(ab)" (str.++ "c(" y))) - -(declare-fun z () String) -(declare-fun w () String) - -(assert (str.contains "c(ab))" (str.++ z "))"))) -(assert (str.contains z "b")) - -(assert (str.contains "c(ab))" (str.++ w "b)"))) -(assert (str.contains w "a")) - - -(declare-fun p () String) -(declare-fun q () String) - -(assert (str.contains "c(aab))" (str.++ "a" p))) -(assert (str.contains p "a")) - -(assert (str.contains "c(abb))" (str.++ q "b"))) -(assert (str.contains q "b")) - -(check-sat) |