diff options
Diffstat (limited to 'test/regress/regress1/strings')
7 files changed, 21 insertions, 30 deletions
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/cmu-disagree-0707-dd.smt2 b/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2 deleted file mode 100644 index c44dfa396..000000000 --- a/test/regress/regress1/strings/cmu-disagree-0707-dd.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-fun url () String) - -(assert -(and -(and -(and -(and - -(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0) - -(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http"))) -(> (str.indexof url ":" 0) 0)) -(>= (- (str.indexof url "#" 2) 2) 0)) -(>= (str.indexof url ":" 0) 0)) -) - -(check-sat) - 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) |