7 files changed, 29 insertions, 5 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 159f87037..d61203ac2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -884,6 +884,7 @@ set(regress_0_tests
   regress0/strings/bug002.smt2
   regress0/strings/bug612.smt2
   regress0/strings/bug613.smt2
+  regress0/strings/code-eval.smt2
   regress0/strings/code-perf.smt2
   regress0/strings/code-sat-neg-one.smt2
   regress0/strings/escchar.smt2
@@ -907,6 +908,7 @@ set(regress_0_tests
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/parser-syms.cvc
   regress0/strings/re.all.smt2
+  regress0/strings/re-syntax.smt2
   regress0/strings/regexp-native-simple.cvc
   regress0/strings/regexp_inclusion.smt2
   regress0/strings/regexp_inclusion_reduction.smt2
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)