diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/strings/idof-sem.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/repl-rewrites2.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress1/strings/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress1/strings/double-replace.smt2 | 3 | ||||
-rw-r--r-- | test/regress/regress1/strings/repl-empty-sem.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress1/strings/repl-soundness-sem.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress1/strings/rew-020618.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/strings/string-unsound-sem.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress2/strings/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 (renamed from test/regress/regress1/strings/cmu-disagree-0707-dd.smt2) | 0 |
10 files changed, 28 insertions, 13 deletions
diff --git a/test/regress/regress0/strings/idof-sem.smt2 b/test/regress/regress0/strings/idof-sem.smt2 index 90dcc83a0..0de8f6a67 100644 --- a/test/regress/regress0/strings/idof-sem.smt2 +++ b/test/regress/regress0/strings/idof-sem.smt2 @@ -1,6 +1,6 @@ (set-logic SLIA) (set-option :strings-exp true) -(set-info :status unsat) +(set-info :status sat) (declare-fun x () String) (assert (not (= (str.indexof x "" 0) (- 1)))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/strings/repl-rewrites2.smt2 b/test/regress/regress0/strings/repl-rewrites2.smt2 index 42699bc8b..e56a8ea44 100644 --- a/test/regress/regress0/strings/repl-rewrites2.smt2 +++ b/test/regress/regress0/strings/repl-rewrites2.smt2 @@ -5,10 +5,11 @@ (declare-fun x () String) (declare-fun y () String) (assert (or -(not (= (str.replace "" "" "c") "")) +(not (= (str.replace "" "" "c") "c")) (not (= (str.replace (str.++ "abc" y) "b" x) (str.++ "a" x "c" y))) (not (= (str.replace "" "abc" "de") "")) (not (= (str.replace "ab" "ab" "de") "de")) -(not (= (str.replace "ab" "" "de") "ab")) +(not (= (str.replace "ab" "" "de") "deab")) +(not (= (str.replace "abb" "b" "de") "adeb")) )) (check-sat) diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am index 493cd5b6d..f6326e0c6 100644 --- a/test/regress/regress1/strings/Makefile.am +++ b/test/regress/regress1/strings/Makefile.am @@ -25,7 +25,6 @@ TESTS = \ bug768.smt2 \ bug799-min.smt2 \ chapman150408.smt2 \ - cmu-disagree-0707-dd.smt2 \ cmu-inc-nlpp-071516.smt2 \ cmu-substr-rw.smt2 \ crash-1019.smt2 \ @@ -73,7 +72,8 @@ TESTS = \ str002.smt2 \ str007.smt2 \ rew-020618.smt2 \ - double-replace.smt2 + double-replace.smt2 \ + string-unsound-sem.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/strings/double-replace.smt2 b/test/regress/regress1/strings/double-replace.smt2 index 0800592d6..bfbc3afc1 100644 --- a/test/regress/regress1/strings/double-replace.smt2 +++ b/test/regress/regress1/strings/double-replace.smt2 @@ -1,7 +1,8 @@ (set-logic SLIA) +(set-option :strings-fmf true) (set-option :strings-exp true) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) (assert (not (= (str.replace (str.replace x y x) x y) x))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress1/strings/repl-empty-sem.smt2 b/test/regress/regress1/strings/repl-empty-sem.smt2 index 61f70bc23..56d4f1b86 100644 --- a/test/regress/regress1/strings/repl-empty-sem.smt2 +++ b/test/regress/regress1/strings/repl-empty-sem.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --strings-exp -; EXPECT: unsat +; EXPECT: sat (set-logic ALL) -(set-info :status unsat) +(set-info :status sat) (declare-fun x () String) (declare-fun z () String) (assert (= (str.len z) 0)) diff --git a/test/regress/regress1/strings/repl-soundness-sem.smt2 b/test/regress/regress1/strings/repl-soundness-sem.smt2 index d56d7945f..f65b3b56a 100644 --- a/test/regress/regress1/strings/repl-soundness-sem.smt2 +++ b/test/regress/regress1/strings/repl-soundness-sem.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --strings-exp -; EXPECT: sat +; EXPECT: unsat (set-logic ALL) -(set-info :status sat) +(set-info :status unsat) (declare-fun x () String) (declare-fun y () String) (assert (and diff --git a/test/regress/regress1/strings/rew-020618.smt2 b/test/regress/regress1/strings/rew-020618.smt2 index 5fb58a272..95dbf4d29 100644 --- a/test/regress/regress1/strings/rew-020618.smt2 +++ b/test/regress/regress1/strings/rew-020618.smt2 @@ -9,7 +9,7 @@ (= (str.++ s s) "A") (not (str.contains s "")) (str.contains "" (str.++ s "A")) -(not (= (str.replace "A" s "A") "A")) +(not (= (str.replace "A" "" "A") "AA")) (not (= (str.prefixof s "A") (str.suffixof s "A"))) (not (str.prefixof s s)) (not (str.prefixof "" s)) diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2 new file mode 100644 index 000000000..771d8d4b0 --- /dev/null +++ b/test/regress/regress1/strings/string-unsound-sem.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () Int) +(assert (and +(not (= (str.replace "A" (int.to.str z) x) (str.++ "A" (str.replace "" (int.to.str z) x)))) +(not (= (str.replace x (str.at x z) "") (str.++ (str.replace (str.++ (str.substr x 0 z) (str.substr x z 1)) (str.substr x z 1) "") (str.substr x (+ 1 z) (str.len x))))) +) +) +(check-sat) diff --git a/test/regress/regress2/strings/Makefile.am b/test/regress/regress2/strings/Makefile.am index 9b397699c..4e6f3aa56 100644 --- a/test/regress/regress2/strings/Makefile.am +++ b/test/regress/regress2/strings/Makefile.am @@ -19,7 +19,8 @@ endif TESTS = \ cmu-dis-0707-3.smt2 \ cmu-prereg-fmf.smt2 \ - cmu-repl-len-nterm.smt2 + cmu-repl-len-nterm.smt2 \ + cmu-disagree-0707-dd.smt2 EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 index c44dfa396..c44dfa396 100644 --- a/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2 +++ b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 |