diff options
Diffstat (limited to 'test/regress/regress0/strings')
-rw-r--r-- | test/regress/regress0/strings/code-eval.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/strings/code-perf.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/code-sat-neg-one.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/re-syntax.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/replaceall-eval.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/strings/std2.6.1.smt2 | 4 |
6 files changed, 27 insertions, 5 deletions
diff --git a/test/regress/regress0/strings/code-eval.smt2 b/test/regress/regress0/strings/code-eval.smt2 new file mode 100644 index 000000000..faa5c174c --- /dev/null +++ b/test/regress/regress0/strings/code-eval.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(assert (< (str.to_code "A") (str.to_code "Z"))) +(assert (= (- 1) (str.to_code "AAA"))) +(assert (= (- 1) (str.to_code ""))) + +(check-sat) diff --git a/test/regress/regress0/strings/code-perf.smt2 b/test/regress/regress0/strings/code-perf.smt2 index 39cab48ce..4d7e22bd3 100644 --- a/test/regress/regress0/strings/code-perf.smt2 +++ b/test/regress/regress0/strings/code-perf.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: sat +(set-info :smt-lib-version 2.5) (set-logic QF_SLIA) (declare-const x0 String) (declare-const x1 String) diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2 index c69276a4f..403319d02 100644 --- a/test/regress/regress0/strings/code-sat-neg-one.smt2 +++ b/test/regress/regress0/strings/code-sat-neg-one.smt2 @@ -1,3 +1,4 @@ +(set-info :smt-lib-version 2.5) (set-logic QF_SLIA) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/re-syntax.smt2 b/test/regress/regress0/strings/re-syntax.smt2 new file mode 100644 index 000000000..4c25a65a4 --- /dev/null +++ b/test/regress/regress0/strings/re-syntax.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) + +(assert (or (str.in_re x re.none) (not (str.in_re x re.all)))) + +(check-sat) diff --git a/test/regress/regress0/strings/replaceall-eval.smt2 b/test/regress/regress0/strings/replaceall-eval.smt2 index 924515901..c118a7dc4 100644 --- a/test/regress/regress0/strings/replaceall-eval.smt2 +++ b/test/regress/regress0/strings/replaceall-eval.smt2 @@ -1,10 +1,11 @@ -(set-info :smt-lib-version 2.5) +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) -(assert (= x (str.replaceall "AABAABBC" "B" "def"))) -(assert (= y (str.replaceall "AABAABBC" "AB" "BA"))) +(assert (= x (str.replace_all "AABAABBC" "B" "def"))) +(assert (= y (str.replace_all "AABAABBC" "AB" "BA"))) (check-sat) diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2 index 3302a29e5..d30cfc83c 100644 --- a/test/regress/regress0/strings/std2.6.1.smt2 +++ b/test/regress/regress0/strings/std2.6.1.smt2 @@ -3,7 +3,7 @@ (set-logic QF_UFSLIA) (set-info :status sat) (declare-fun x () String) -(assert (str.in-re x (str.to-re "A"))) +(assert (str.in_re x (str.to_re "A"))) (declare-fun y () Int) -(assert (= (str.to-int (str.from-int y)) y)) +(assert (= (str.to_int (str.from_int y)) y)) (check-sat) |