Initial support for string standard in smt lib 2.6 (#1848)

21 files changed, 28 insertions, 7 deletions

diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
index 4b1cad8f6..a3cca23a2 100644
--- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)
diff --git a/test/regress/regress1/strings/bug615.smt2 b/test/regress/regress1/strings/bug615.smt2
index 86cc592fb..673b0dbd0 100644
--- a/test/regress/regress1/strings/bug615.smt2
+++ b/test/regress/regress1/strings/bug615.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/bug686dd.smt2 b/test/regress/regress1/strings/bug686dd.smt2
index 7c923654d..0cb9fac26 100644
--- a/test/regress/regress1/strings/bug686dd.smt2
+++ b/test/regress/regress1/strings/bug686dd.smt2
@@ -1,7 +1,8 @@
+(set-info :smt-lib-version 2.5)
 (set-logic UFDTSLIA)
 (set-info :status sat)
 
-(declare-datatypes ((T 0)) ( ((TC (TCb String))) ) )
+(declare-datatypes () ((T (TC (TCb String)))))
 
 (declare-fun root5 () String)
 (declare-fun root6 () T)
diff --git a/test/regress/regress1/strings/bug799-min.smt2 b/test/regress/regress1/strings/bug799-min.smt2
index 06acffc97..0cd15af4e 100644
--- a/test/regress/regress1/strings/bug799-min.smt2
+++ b/test/regress/regress1/strings/bug799-min.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --incremental --strings-exp
 ; EXPECT: sat
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/fmf001.smt2 b/test/regress/regress1/strings/fmf001.smt2
index 6081c8e06..71ae63e87 100644
--- a/test/regress/regress1/strings/fmf001.smt2
+++ b/test/regress/regress1/strings/fmf001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2
index d52dae2d2..ab3dc2ae2 100644
--- a/test/regress/regress1/strings/fmf002.smt2
+++ b/test/regress/regress1/strings/fmf002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2
index 81e7672da..bf5cb7669 100644
--- a/test/regress/regress1/strings/issue1105.smt2
+++ b/test/regress/regress1/strings/issue1105.smt2
@@ -1,9 +1,10 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
-(declare-datatype Val (
+(declare-datatypes () ((Val
     (Str (str String))
-    (Num (num Int))))
+    (Num (num Int)))))
 
 (declare-const var0 Val)
 (assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1))))
diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2
index 04775d61c..20c2e6aa4 100644
--- a/test/regress/regress1/strings/kaluza-fl.smt2
+++ b/test/regress/regress1/strings/kaluza-fl.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/norn-360.smt2 b/test/regress/regress1/strings/norn-360.smt2
index 573dcbe01..20ab0b338 100644
--- a/test/regress/regress1/strings/norn-360.smt2
+++ b/test/regress/regress1/strings/norn-360.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2
index 48d889847..47c218179 100644
--- a/test/regress/regress1/strings/norn-ab.smt2
+++ b/test/regress/regress1/strings/norn-ab.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
 (assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
 (assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/norn-nel-bug-052116.smt2 b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
index f0c2534a1..9f06152f7 100644
--- a/test/regress/regress1/strings/norn-nel-bug-052116.smt2
+++ b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/norn-simp-rew-sat.smt2 b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
index 01a102bf9..1336d3bfc 100644
--- a/test/regress/regress1/strings/norn-simp-rew-sat.smt2
+++ b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (str.to.re "a"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2
index 88d5ec10c..add60d534 100644
--- a/test/regress/regress1/strings/pierre150331.smt2
+++ b/test/regress/regress1/strings/pierre150331.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)

 (set-logic SLIA)

 (set-info :status sat)

 (set-info :smt-lib-version 2.5)

@@ -10,4 +11,4 @@
 (declare-fun s1() String)

 (declare-fun s2() String)

 (assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) )

-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/regexp001.smt2 b/test/regress/regress1/strings/regexp001.smt2
index 62c142d1d..142ff679d 100644
--- a/test/regress/regress1/strings/regexp001.smt2
+++ b/test/regress/regress1/strings/regexp001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/regexp002.smt2 b/test/regress/regress1/strings/regexp002.smt2
index a8bd2187a..f109a484e 100644
--- a/test/regress/regress1/strings/regexp002.smt2
+++ b/test/regress/regress1/strings/regexp002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/regexp003.smt2 b/test/regress/regress1/strings/regexp003.smt2
index 7696838fe..7c05b422f 100644
--- a/test/regress/regress1/strings/regexp003.smt2
+++ b/test/regress/regress1/strings/regexp003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 9915504ae..967e564ce 100644
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2
index 771d8d4b0..44591b47b 100644
--- a/test/regress/regress1/strings/string-unsound-sem.smt2
+++ b/test/regress/regress1/strings/string-unsound-sem.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2
index 0df0f20b0..458ac75fe 100644
--- a/test/regress/regress1/strings/type002.smt2
+++ b/test/regress/regress1/strings/type002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2
index c2d4792cc..4185041f7 100644
--- a/test/regress/regress1/strings/type003.smt2
+++ b/test/regress/regress1/strings/type003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/username_checker_min.smt2 b/test/regress/regress1/strings/username_checker_min.smt2
index 2f1c35844..f6c152a2a 100644
--- a/test/regress/regress1/strings/username_checker_min.smt2
+++ b/test/regress/regress1/strings/username_checker_min.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)