diff options
Diffstat (limited to 'test/regress/regress0/strings')
40 files changed, 90 insertions, 89 deletions
diff --git a/test/regress/regress0/strings/bidir_star.smt2 b/test/regress/regress0/strings/bidir_star.smt2 index 7303d138f..8a13ed085 100644 --- a/test/regress/regress0/strings/bidir_star.smt2 +++ b/test/regress/regress0/strings/bidir_star.smt2 @@ -2,7 +2,7 @@ (set-logic SLIA) (declare-fun a () String) (assert (>= (str.len a) 2)) -(assert (str.in.re a (re.+ (re.range "0" "1")))) -(assert (<= 3 (str.to.int (str.substr a (+ (- 2) (str.len a)) 1)))) +(assert (str.in_re a (re.+ (re.range "0" "1")))) +(assert (<= 3 (str.to_int (str.substr a (+ (- 2) (str.len a)) 1)))) (set-info :status unsat) (check-sat) diff --git a/test/regress/regress0/strings/bug001.smt2 b/test/regress/regress0/strings/bug001.smt2 index cdeebd20b..a8d2d8992 100644 --- a/test/regress/regress0/strings/bug001.smt2 +++ b/test/regress/regress0/strings/bug001.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/regress0/strings/char-representations.smt2 b/test/regress/regress0/strings/char-representations.smt2 index aaf119ab4..1b3cef25a 100644 --- a/test/regress/regress0/strings/char-representations.smt2 +++ b/test/regress/regress0/strings/char-representations.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 +; COMMAND-LINE: --lang=smt2.6 ; EXPECT: sat (set-logic SLIA) (set-info :status sat) diff --git a/test/regress/regress0/strings/code-eval.smt2 b/test/regress/regress0/strings/code-eval.smt2 index faa5c174c..bc5f96494 100644 --- a/test/regress/regress0/strings/code-eval.smt2 +++ b/test/regress/regress0/strings/code-eval.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 +; COMMAND-LINE: --lang=smt2.6 ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/regress0/strings/code-perf.smt2 b/test/regress/regress0/strings/code-perf.smt2 index 4d7e22bd3..e2b41c67f 100644 --- a/test/regress/regress0/strings/code-perf.smt2 +++ b/test/regress/regress0/strings/code-perf.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: sat -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (declare-const x0 String) (declare-const x1 String) @@ -24,17 +24,17 @@ (declare-const y8 Int) (declare-const y9 Int) (declare-const y10 Int) -(assert (and (= y0 (str.code x0)) (>= y0 (str.code "0")) (<= y0 (str.code "9")))) -(assert (and (= y1 (str.code x1)) (>= y1 (str.code "0")) (<= y1 (str.code "9")))) -(assert (and (= y2 (str.code x2)) (>= y2 (str.code "0")) (<= y2 (str.code "9")))) -(assert (and (= y3 (str.code x3)) (>= y3 (str.code "0")) (<= y3 (str.code "9")))) -(assert (and (= y4 (str.code x4)) (>= y4 (str.code "0")) (<= y4 (str.code "9")))) -(assert (and (= y5 (str.code x5)) (>= y5 (str.code "0")) (<= y5 (str.code "9")))) -(assert (and (= y6 (str.code x6)) (>= y6 (str.code "0")) (<= y6 (str.code "9")))) -(assert (and (= y7 (str.code x7)) (>= y7 (str.code "0")) (<= y7 (str.code "9")))) -(assert (and (= y8 (str.code x8)) (>= y8 (str.code "0")) (<= y8 (str.code "9")))) -(assert (and (= y9 (str.code x9)) (>= y9 (str.code "0")) (<= y9 (str.code "9")))) -(assert (and (= y10 (str.code x10)) (>= y10 (str.code "0")) (<= y10 (str.code "9")))) +(assert (and (= y0 (str.to_code x0)) (>= y0 (str.to_code "0")) (<= y0 (str.to_code "9")))) +(assert (and (= y1 (str.to_code x1)) (>= y1 (str.to_code "0")) (<= y1 (str.to_code "9")))) +(assert (and (= y2 (str.to_code x2)) (>= y2 (str.to_code "0")) (<= y2 (str.to_code "9")))) +(assert (and (= y3 (str.to_code x3)) (>= y3 (str.to_code "0")) (<= y3 (str.to_code "9")))) +(assert (and (= y4 (str.to_code x4)) (>= y4 (str.to_code "0")) (<= y4 (str.to_code "9")))) +(assert (and (= y5 (str.to_code x5)) (>= y5 (str.to_code "0")) (<= y5 (str.to_code "9")))) +(assert (and (= y6 (str.to_code x6)) (>= y6 (str.to_code "0")) (<= y6 (str.to_code "9")))) +(assert (and (= y7 (str.to_code x7)) (>= y7 (str.to_code "0")) (<= y7 (str.to_code "9")))) +(assert (and (= y8 (str.to_code x8)) (>= y8 (str.to_code "0")) (<= y8 (str.to_code "9")))) +(assert (and (= y9 (str.to_code x9)) (>= y9 (str.to_code "0")) (<= y9 (str.to_code "9")))) +(assert (and (= y10 (str.to_code x10)) (>= y10 (str.to_code "0")) (<= y10 (str.to_code "9")))) (assert (= (str.len x0) 1)) (assert (= (str.len x1) 1)) (assert (= (str.len x2) 1)) diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2 index 403319d02..3e7161328 100644 --- a/test/regress/regress0/strings/code-sat-neg-one.smt2 +++ b/test/regress/regress0/strings/code-sat-neg-one.smt2 @@ -1,8 +1,8 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) (assert (not (= x y))) -(assert (= (str.code x) (str.code y))) +(assert (= (str.to_code x) (str.to_code y))) (check-sat) diff --git a/test/regress/regress0/strings/complement-simple.smt2 b/test/regress/regress0/strings/complement-simple.smt2 index c19699448..d86fcd225 100644 --- a/test/regress/regress0/strings/complement-simple.smt2 +++ b/test/regress/regress0/strings/complement-simple.smt2 @@ -1,5 +1,5 @@ (set-logic SLIA) (set-info :status sat) (declare-fun x () String) -(assert (str.in.re x (re.comp (str.to.re "ABC")))) +(assert (str.in_re x (re.comp (str.to_re "ABC")))) (check-sat) diff --git a/test/regress/regress0/strings/escchar_25.smt2 b/test/regress/regress0/strings/escchar_25.smt2 index af93a7ae5..a8a7c242f 100644 --- a/test/regress/regress0/strings/escchar_25.smt2 +++ b/test/regress/regress0/strings/escchar_25.smt2 @@ -1,6 +1,6 @@ (set-logic QF_S) (set-info :status sat) -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (declare-fun x () String) (declare-const I Int) diff --git a/test/regress/regress0/strings/from_code.smt2 b/test/regress/regress0/strings/from_code.smt2 index ecde829ec..c9b49a931 100644 --- a/test/regress/regress0/strings/from_code.smt2 +++ b/test/regress/regress0/strings/from_code.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 +; COMMAND-LINE: --lang=smt2.6 ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: sat diff --git a/test/regress/regress0/strings/gen-esc-seq.smt2 b/test/regress/regress0/strings/gen-esc-seq.smt2 index 59f66046f..19edd7fc0 100644 --- a/test/regress/regress0/strings/gen-esc-seq.smt2 +++ b/test/regress/regress0/strings/gen-esc-seq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-models --lang=smt2.6.1 +; COMMAND-LINE: --produce-models --lang=smt2.6 ; EXPECT: sat ; EXPECT: ((x "\u{5c}u1000")) (set-logic ALL) diff --git a/test/regress/regress0/strings/is_digit_simple.smt2 b/test/regress/regress0/strings/is_digit_simple.smt2 index d95a22078..d69ec6b21 100644 --- a/test/regress/regress0/strings/is_digit_simple.smt2 +++ b/test/regress/regress0/strings/is_digit_simple.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 +; COMMAND-LINE: --lang=smt2.6 ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2 index 0b581994c..3200c815d 100644 --- a/test/regress/regress0/strings/issue1189.smt2 +++ b/test/regress/regress0/strings/issue1189.smt2 @@ -1,7 +1,7 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic ALL_SUPPORTED) (set-info :status unsat) (set-option :strings-exp true) (declare-const x Int) -(assert (str.contains (str.++ "some text" (int.to.str x) "tor") "vector")) +(assert (str.contains (str.++ "some text" (str.from_int x) "tor") "vector")) (check-sat) diff --git a/test/regress/regress0/strings/issue2958.smt2 b/test/regress/regress0/strings/issue2958.smt2 index 7ed5ef7f3..99d8462c3 100644 --- a/test/regress/regress0/strings/issue2958.smt2 +++ b/test/regress/regress0/strings/issue2958.smt2 @@ -1,7 +1,7 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-info :status unsat) (declare-const x String) (assert (not (str.prefixof "ab" x))) -(assert (str.in.re (str.substr x 0 2) (re.++ (str.to.re "ab") (re.* (str.to.re "dcab"))))) +(assert (str.in_re (str.substr x 0 2) (re.++ (str.to_re "ab") (re.* (str.to_re "dcab"))))) (check-sat) diff --git a/test/regress/regress0/strings/issue3440.smt2 b/test/regress/regress0/strings/issue3440.smt2 index 7eb3419f2..32f6bf90f 100644 --- a/test/regress/regress0/strings/issue3440.smt2 +++ b/test/regress/regress0/strings/issue3440.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-strings-lazy-pp ; EXPECT: sat -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_S) (set-info :status sat) (declare-fun a () String) diff --git a/test/regress/regress0/strings/issue3497.smt2 b/test/regress/regress0/strings/issue3497.smt2 index c804de820..99597dffa 100644 --- a/test/regress/regress0/strings/issue3497.smt2 +++ b/test/regress/regress0/strings/issue3497.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress0/strings/issue3657-evalLeq.smt2 b/test/regress/regress0/strings/issue3657-evalLeq.smt2 index a557f4e62..91295f73a 100644 --- a/test/regress/regress0/strings/issue3657-evalLeq.smt2 +++ b/test/regress/regress0/strings/issue3657-evalLeq.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic ALL) (set-info :status sat) (assert (not (str.< "\xe8" "\x19"))) diff --git a/test/regress/regress0/strings/issue4070.smt2 b/test/regress/regress0/strings/issue4070.smt2 index 2de58c4d2..a629c30ec 100644 --- a/test/regress/regress0/strings/issue4070.smt2 +++ b/test/regress/regress0/strings/issue4070.smt2 @@ -2,5 +2,5 @@ (set-logic QF_S) (declare-fun a () String) (declare-fun b () String) -(assert (str.in.re a (re.++ (str.to.re b) (re.* re.allchar)))) +(assert (str.in_re a (re.++ (str.to_re b) (re.* re.allchar)))) (check-sat) diff --git a/test/regress/regress0/strings/issue4376.smt2 b/test/regress/regress0/strings/issue4376.smt2 index f6dd88059..3a7088c5b 100644 --- a/test/regress/regress0/strings/issue4376.smt2 +++ b/test/regress/regress0/strings/issue4376.smt2 @@ -7,5 +7,5 @@ (declare-const Str11 String) (declare-const Str15 String) (assert (= (str.++ Str1 "ijruldtzyp") Str15)) -(assert (= (str.++ (str.++ Str1 "ijruldtzyp") Str11 (int.to.str i0)) Str15 Str9)) +(assert (= (str.++ (str.++ Str1 "ijruldtzyp") Str11 (str.from_int i0)) Str15 Str9)) (check-sat) diff --git a/test/regress/regress0/strings/itos-entail.smt2 b/test/regress/regress0/strings/itos-entail.smt2 index f9dcf4c77..aca5e4f6a 100644 --- a/test/regress/regress0/strings/itos-entail.smt2 +++ b/test/regress/regress0/strings/itos-entail.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic ALL) (set-info :status sat) (set-option :strings-exp true) @@ -6,6 +6,6 @@ (declare-fun y () String) (declare-fun z () String) -(assert (str.contains "ABCD" (str.++ y (int.to.str x) z))) +(assert (str.contains "ABCD" (str.++ y (str.from_int x) z))) (check-sat) diff --git a/test/regress/regress0/strings/large-model.smt2 b/test/regress/regress0/strings/large-model.smt2 index ca52e816b..74b781c82 100644 --- a/test/regress/regress0/strings/large-model.smt2 +++ b/test/regress/regress0/strings/large-model.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 --check-models +; COMMAND-LINE: --lang=smt2.6 --check-models ; EXPECT: (error "Cannot generate model with string whose length exceeds UINT32_MAX") ; EXIT: 1 (set-logic SLIA) diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2 index 09fd80a7b..d646a8930 100644 --- a/test/regress/regress0/strings/leadingzero001.smt2 +++ b/test/regress/regress0/strings/leadingzero001.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_S) (set-option :strings-exp true) (set-info :status sat) @@ -6,7 +6,7 @@ (declare-fun Y () String) (assert (= Y "0001")) -;(assert (= (str.to.int Y) (- 1))) -(assert (= (str.to.int Y) 1)) +;(assert (= (str.to_int Y) (- 1))) +(assert (= (str.to_int Y) 1)) (check-sat) diff --git a/test/regress/regress0/strings/loop-wrong-sem.smt2 b/test/regress/regress0/strings/loop-wrong-sem.smt2 index d0dd3fcb2..32ec26c0a 100644 --- a/test/regress/regress0/strings/loop-wrong-sem.smt2 +++ b/test/regress/regress0/strings/loop-wrong-sem.smt2 @@ -1,4 +1,4 @@ (set-logic ALL) (set-info :status unsat) -(assert (str.in.re "" ((_ re.loop 1 0) (str.to.re "")))) +(assert (str.in_re "" ((_ re.loop 1 0) (str.to_re "")))) (check-sat) diff --git a/test/regress/regress0/strings/model-code-point.smt2 b/test/regress/regress0/strings/model-code-point.smt2 index 1200ae704..86cb24fc7 100644 --- a/test/regress/regress0/strings/model-code-point.smt2 +++ b/test/regress/regress0/strings/model-code-point.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 --produce-models +; COMMAND-LINE: --lang=smt2.6 --produce-models ; EXPECT: sat ; EXPECT: ((x "\u{a}")) ; EXPECT: ((y "\u{7f}")) diff --git a/test/regress/regress0/strings/model-friendly.smt2 b/test/regress/regress0/strings/model-friendly.smt2 index 985ffaa62..21a89c00c 100644 --- a/test/regress/regress0/strings/model-friendly.smt2 +++ b/test/regress/regress0/strings/model-friendly.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 --produce-models +; COMMAND-LINE: --lang=smt2.6 --produce-models ; EXPECT: sat ; EXPECT: ((x "AAAAA")) (set-logic ALL) diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2 index 1830dd882..be759a885 100644 --- a/test/regress/regress0/strings/norn-31.smt2 +++ b/test/regress/regress0/strings/norn-31.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status unsat) @@ -17,8 +17,8 @@ (declare-fun var_11 () String) (declare-fun var_12 () String) -(assert (str.in.re var_1 (re.* (re.range "a" "u")))) -(assert (str.in.re var_1 (re.++ (re.* (str.to.re "a")) (str.to.re "b")))) -(assert (str.in.re var_1 (re.++ (re.++ (re.++ (re.* (re.union (str.to.re "a") (str.to.re "b"))) (str.to.re "b")) (str.to.re "a")) (re.* (re.union (str.to.re "a") (str.to.re "b")))))) -(assert (not (str.in.re "" re.nostr))) +(assert (str.in_re var_1 (re.* (re.range "a" "u")))) +(assert (str.in_re var_1 (re.++ (re.* (str.to_re "a")) (str.to_re "b")))) +(assert (str.in_re var_1 (re.++ (re.++ (re.++ (re.* (re.union (str.to_re "a") (str.to_re "b"))) (str.to_re "b")) (str.to_re "a")) (re.* (re.union (str.to_re "a") (str.to_re "b")))))) +(assert (not (str.in_re "" re.none))) (check-sat) diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2 index d729fe5d0..4ef281ce9 100644 --- a/test/regress/regress0/strings/norn-simp-rew.smt2 +++ b/test/regress/regress0/strings/norn-simp-rew.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status unsat) @@ -17,14 +17,14 @@ (declare-fun var_11 () String) (declare-fun var_12 () String) -(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))) -(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a"))))))) -(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "b"))) (str.to.re "a")))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "b"))))))) -(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))) (re.union (str.to.re "b") (str.to.re "a"))))) -(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "z")) (str.to.re "b")))))) -(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b")))) -(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u")))) -(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"))))) +(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (re.union (str.to_re "z") (str.to_re "a")) (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "b")) (re.union (str.to_re "z") (str.to_re "a")))))) (re.++ (str.to_re "b") (re.* (str.to_re "b")))))) +(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to_re "a") (re.++ (str.to_re "b") (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a"))) (str.to_re "z"))))) (re.++ (str.to_re "b") (re.* (re.union (str.to_re "b") (str.to_re "a"))))))) +(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to_re "b") (re.++ (re.* (re.union (str.to_re "z") (str.to_re "b"))) (str.to_re "a")))) (re.++ (str.to_re "b") (re.* (re.union (str.to_re "z") (str.to_re "b"))))))) +(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to_re "z") (re.++ (re.union (str.to_re "b") (str.to_re "a")) (re.union (str.to_re "z") (str.to_re "b"))))) (re.union (str.to_re "b") (str.to_re "a"))))) +(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "z")) (str.to_re "b")))))) +(assert (str.in_re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to_re "b") (str.to_re "z"))) (str.to_re "b")))) +(assert (str.in_re (str.++ "a" var_8 ) (re.* (re.range "a" "u")))) +(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) diff --git a/test/regress/regress0/strings/re-syntax.smt2 b/test/regress/regress0/strings/re-syntax.smt2 index 4c25a65a4..f073884b8 100644 --- a/test/regress/regress0/strings/re-syntax.smt2 +++ b/test/regress/regress0/strings/re-syntax.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 +; COMMAND-LINE: --lang=smt2.6 ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/regress0/strings/re.all.smt2 b/test/regress/regress0/strings/re.all.smt2 index 5200b924f..d17a0d049 100644 --- a/test/regress/regress0/strings/re.all.smt2 +++ b/test/regress/regress0/strings/re.all.smt2 @@ -1,6 +1,6 @@ (set-logic QF_SLIA) (set-info :status unsat) (declare-const x String) -(assert (str.in.re x (re.++ (str.to.re "abc") re.all))) +(assert (str.in_re x (re.++ (str.to_re "abc") re.all))) (assert (not (str.prefixof "abc" x))) (check-sat) diff --git a/test/regress/regress0/strings/re_diff.smt2 b/test/regress/regress0/strings/re_diff.smt2 index d63731acb..a20c5be7e 100644 --- a/test/regress/regress0/strings/re_diff.smt2 +++ b/test/regress/regress0/strings/re_diff.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 +; COMMAND-LINE: --lang=smt2.6 ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/regress0/strings/regexp_inclusion.smt2 b/test/regress/regress0/strings/regexp_inclusion.smt2 index c5c68a408..648a1b111 100644 --- a/test/regress/regress0/strings/regexp_inclusion.smt2 +++ b/test/regress/regress0/strings/regexp_inclusion.smt2 @@ -4,10 +4,10 @@ (declare-const actionName String) (assert -(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (str.to.re "foobar") (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar)))) +(str.in_re actionName (re.++ (str.to_re "wiz") (re.* re.allchar) (str.to_re "foobar") (re.* re.allchar) (str.to_re "baz/") (re.* re.allchar)))) (assert (not -(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (re.++ (str.to.re "foo") re.allchar (str.to.re "ar")) (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar))) +(str.in_re actionName (re.++ (str.to_re "wiz") (re.* re.allchar) (re.++ (str.to_re "foo") re.allchar (str.to_re "ar")) (re.* re.allchar) (str.to_re "baz/") (re.* re.allchar))) )) (check-sat) diff --git a/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 index c10c287bb..20ac8f4e4 100644 --- a/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 +++ b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 @@ -4,11 +4,11 @@ (declare-const x String) (declare-const y String) -(assert (str.in.re x (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar")))) -(assert (str.in.re x (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar")))) +(assert (str.in_re x (re.++ (str.to_re "bar") (re.* re.allchar) (str.to_re "bar")))) +(assert (str.in_re x (re.++ (str.to_re "ba") re.allchar (re.* re.allchar) (str.to_re "bar")))) -(assert (not (str.in.re y (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar"))))) -(assert (not (str.in.re y (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar"))))) +(assert (not (str.in_re y (re.++ (str.to_re "bar") (re.* re.allchar) (str.to_re "bar"))))) +(assert (not (str.in_re y (re.++ (str.to_re "ba") re.allchar (re.* re.allchar) (str.to_re "bar"))))) (assert (not (= y ""))) (check-sat) diff --git a/test/regress/regress0/strings/replace-const.smt2 b/test/regress/regress0/strings/replace-const.smt2 index a7f225e33..8b1b182e3 100644 --- a/test/regress/regress0/strings/replace-const.smt2 +++ b/test/regress/regress0/strings/replace-const.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic ALL) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/replaceall-eval.smt2 b/test/regress/regress0/strings/replaceall-eval.smt2 index c118a7dc4..f2edfe3fb 100644 --- a/test/regress/regress0/strings/replaceall-eval.smt2 +++ b/test/regress/regress0/strings/replaceall-eval.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=smt2.6.1 +; COMMAND-LINE: --lang=smt2.6 ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/regress0/strings/rewrites-re-concat.smt2 b/test/regress/regress0/strings/rewrites-re-concat.smt2 index fe6691e73..f2004204a 100644 --- a/test/regress/regress0/strings/rewrites-re-concat.smt2 +++ b/test/regress/regress0/strings/rewrites-re-concat.smt2 @@ -1,20 +1,20 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic SLIA) (set-info :status unsat) (declare-fun x () String) -(assert (str.in.re x (re.++ (str.to.re "baa") (re.* (str.to.re "a")) (re.* (str.to.re "c"))))) +(assert (str.in_re x (re.++ (str.to_re "baa") (re.* (str.to_re "a")) (re.* (str.to_re "c"))))) (declare-fun y () String) (assert (< (str.len y) 2)) (assert (or -(not (str.in.re x (re.++ (str.to.re "baa") (re.* (str.to.re "a")) (re.* (str.to.re "a")) (re.* (str.to.re "c"))))) -(not (str.in.re x (re.++ (str.to.re "ba") (str.to.re "") (re.* (str.to.re "a")) (str.to.re "a") (re.* (str.to.re "c"))))) -(not (str.in.re x (re.++ (str.to.re "b") (re.* (str.to.re "a")) (str.to.re "a") (re.* (str.to.re "a")) (str.to.re "a") (re.* (str.to.re "c"))))) +(not (str.in_re x (re.++ (str.to_re "baa") (re.* (str.to_re "a")) (re.* (str.to_re "a")) (re.* (str.to_re "c"))))) +(not (str.in_re x (re.++ (str.to_re "ba") (str.to_re "") (re.* (str.to_re "a")) (str.to_re "a") (re.* (str.to_re "c"))))) +(not (str.in_re x (re.++ (str.to_re "b") (re.* (str.to_re "a")) (str.to_re "a") (re.* (str.to_re "a")) (str.to_re "a") (re.* (str.to_re "c"))))) -(str.in.re y (re.++ re.allchar re.allchar (re.* re.allchar) re.allchar)) -(str.in.re y (re.++ re.allchar re.allchar re.allchar)) +(str.in_re y (re.++ re.allchar re.allchar (re.* re.allchar) re.allchar)) +(str.in_re y (re.++ re.allchar re.allchar re.allchar)) ) ) diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2 index 15954525f..be9f18681 100644 --- a/test/regress/regress0/strings/rewrites-v2.smt2 +++ b/test/regress/regress0/strings/rewrites-v2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic SLIA) (set-info :status unsat) (declare-fun x () String) @@ -9,8 +9,8 @@ ; these should all rewrite to false (assert (or -(str.contains "abcdef0ghij1abced" (str.++ "g" (int.to.str (str.len z)) x "a" y (int.to.str (+ (str.len z) 1)))) -(str.contains "abc23cd" (str.++ (int.to.str (str.len z)) (int.to.str (str.len z)) (int.to.str (str.len z)))) +(str.contains "abcdef0ghij1abced" (str.++ "g" (str.from_int (str.len z)) x "a" y (str.from_int (+ (str.len z) 1)))) +(str.contains "abc23cd" (str.++ (str.from_int (str.len z)) (str.from_int (str.len z)) (str.from_int (str.len z)))) (not (str.contains (str.++ x "ab" y) (str.++ "b" (str.substr y 0 4)))) (not (str.contains (str.++ x "ab" y) (str.++ (str.substr x 5 (str.len x)) "a"))) (str.contains (str.++ x y) (str.++ x "a" y)) diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2 index d30cfc83c..8881f874d 100644 --- a/test/regress/regress0/strings/std2.6.1.smt2 +++ b/test/regress/regress0/strings/std2.6.1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --lang=smt2.6.1 +; COMMAND-LINE: --strings-exp --lang=smt2.6 ; EXPECT: sat (set-logic QF_UFSLIA) (set-info :status sat) diff --git a/test/regress/regress0/strings/strip-endpoint-itos.smt2 b/test/regress/regress0/strings/strip-endpoint-itos.smt2 index c8d8c5af3..4f098e319 100644 --- a/test/regress/regress0/strings/strip-endpoint-itos.smt2 +++ b/test/regress/regress0/strings/strip-endpoint-itos.smt2 @@ -1,7 +1,7 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status sat) (declare-fun x () Int) -(assert (str.contains "Ducati100" (int.to.str x))) +(assert (str.contains "Ducati100" (str.from_int x))) (check-sat) diff --git a/test/regress/regress0/strings/tolower-rrs.smt2 b/test/regress/regress0/strings/tolower-rrs.smt2 index 7b8b393cd..217255807 100644 --- a/test/regress/regress0/strings/tolower-rrs.smt2 +++ b/test/regress/regress0/strings/tolower-rrs.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic ALL) (set-info :status unsat) (declare-fun x () String) @@ -9,7 +9,7 @@ (assert (or (not (= (str.tolower (str.toupper (str.tolower x))) (str.tolower x))) (not (= (str.tolower (str.++ x "A")) (str.++ (str.tolower x) "a"))) -(not (= (str.tolower (int.to.str y)) (int.to.str y))) +(not (= (str.tolower (str.from_int y)) (str.from_int y))) )) (check-sat) diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2 index 36a6aaec1..168d066ea 100644 --- a/test/regress/regress0/strings/type001.smt2 +++ b/test/regress/regress0/strings/type001.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-info :status sat) (set-option :strings-exp true) @@ -10,13 +10,13 @@ (declare-fun z () String) ;big num test -(assert (= x (int.to.str 4785582390527685649))) +(assert (= x (str.from_int 4785582390527685649))) ;should be "" -(assert (= y (int.to.str (- 9)))) +(assert (= y (str.from_int (- 9)))) ;big num -(assert (= i (str.to.int "783914785582390527685649"))) +(assert (= i (str.to_int "783914785582390527685649"))) ;should be -1 -(assert (= j (str.to.int "-783914785582390527685649"))) +(assert (= j (str.to_int "-783914785582390527685649"))) (check-sat) diff --git a/test/regress/regress0/strings/unicode-esc.smt2 b/test/regress/regress0/strings/unicode-esc.smt2 index 02b313d4a..4039ecd0a 100644 --- a/test/regress/regress0/strings/unicode-esc.smt2 +++ b/test/regress/regress0/strings/unicode-esc.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --lang=smt2.6.1 +; COMMAND-LINE: --strings-exp --lang=smt2.6 ; EXPECT: sat (set-logic ALL) |