diff options
Diffstat (limited to 'test/regress')
30 files changed, 48 insertions, 11 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index f8a32046f..3674e42bb 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -788,6 +788,7 @@ REG0_TESTS = \ regress0/strings/norn-simp-rew.smt2 \ regress0/strings/repl-rewrites2.smt2 \ regress0/strings/rewrites-v2.smt2 \ + regress0/strings/std2.6.1.smt2 \ regress0/strings/str003.smt2 \ regress0/strings/str004.smt2 \ regress0/strings/str005.smt2 \ diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2 index f8a481e14..fd60089fd 100644 --- a/test/regress/regress0/strings/bug002.smt2 +++ b/test/regress/regress0/strings/bug002.smt2 @@ -1,5 +1,5 @@ -(set-logic ASLIA) (set-info :smt-lib-version 2.0) +(set-logic ASLIA) (set-option :strings-exp true) (set-info :status sat) @@ -7,4 +7,4 @@ (define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) ) ) ) (assert (not (strinre "6O\1\127\n?"))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2 index fae641ea8..0b581994c 100644 --- a/test/regress/regress0/strings/issue1189.smt2 +++ b/test/regress/regress0/strings/issue1189.smt2 @@ -1,3 +1,4 @@ +(set-info :smt-lib-version 2.5) (set-logic ALL_SUPPORTED) (set-info :status unsat) (set-option :strings-exp true) diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2 index 2889348c1..09fd80a7b 100644 --- a/test/regress/regress0/strings/leadingzero001.smt2 +++ b/test/regress/regress0/strings/leadingzero001.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/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2 index 4698f966f..1830dd882 100644 --- a/test/regress/regress0/strings/norn-31.smt2 +++ b/test/regress/regress0/strings/norn-31.smt2 @@ -1,3 +1,4 @@ +(set-info :smt-lib-version 2.5) (set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status unsat) diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2 index 45f7ede94..d729fe5d0 100644 --- a/test/regress/regress0/strings/norn-simp-rew.smt2 +++ b/test/regress/regress0/strings/norn-simp-rew.smt2 @@ -1,3 +1,4 @@ +(set-info :smt-lib-version 2.5) (set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status unsat) @@ -26,4 +27,4 @@ (assert (str.in.re var_8 (re.* (re.range "a" "u")))) (assert (str.in.re var_7 (re.* (re.range "a" "u")))) (assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u"))))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2 index 7e285b51a..ce2f140ae 100644 --- a/test/regress/regress0/strings/rewrites-v2.smt2 +++ b/test/regress/regress0/strings/rewrites-v2.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +(set-info :smt-lib-version 2.5) (set-logic SLIA) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2 new file mode 100644 index 000000000..3302a29e5 --- /dev/null +++ b/test/regress/regress0/strings/std2.6.1.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp --lang=smt2.6.1 +; EXPECT: sat +(set-logic QF_UFSLIA) +(set-info :status sat) +(declare-fun x () String) +(assert (str.in-re x (str.to-re "A"))) +(declare-fun y () Int) +(assert (= (str.to-int (str.from-int y)) y)) +(check-sat) diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2 index 77eabcccc..89191ac34 100644 --- a/test/regress/regress0/strings/type001.smt2 +++ b/test/regress/regress0/strings/type001.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) @@ -18,4 +19,4 @@ ;should be -1 (assert (= j (str.to.int "-783914785582390527685649"))) -(check-sat)
\ No newline at end of file +(check-sat) 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) |