Update semantics for string indexof and replace (#1630)

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