diff options
Diffstat (limited to 'test/regress/regress2')
23 files changed, 27 insertions, 40 deletions
diff --git a/test/regress/regress2/DTP_k2_n35_c175_s15.smt2 b/test/regress/regress2/DTP_k2_n35_c175_s15.smt2 index 20f4bf5a9..9a20c82ac 100644 --- a/test/regress/regress2/DTP_k2_n35_c175_s15.smt2 +++ b/test/regress/regress2/DTP_k2_n35_c175_s15.smt2 @@ -5,7 +5,7 @@ http://www.ai.dist.unige.it/Tsat for more information. Translated into SMT-LIB format by Albert Oliveras. |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "random") (set-info :status sat) (declare-fun x10 () Int) diff --git a/test/regress/regress2/arith/miplib-opt1217--27.smt2 b/test/regress/regress2/arith/miplib-opt1217--27.smt2 index 2adcdd3a9..802839bb8 100644 --- a/test/regress/regress2/arith/miplib-opt1217--27.smt2 +++ b/test/regress/regress2/arith/miplib-opt1217--27.smt2 @@ -6,7 +6,7 @@ Relaxation of the Mixed-Integer Programming optimization problem opt1217 from the MIPLIB (http://miplib.zib.de/) by Enric Rodriguez-Carbonell (erodri@lsi.upc.edu) |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun tmp766 () Real) diff --git a/test/regress/regress2/bug394.smt2 b/test/regress/regress2/bug394.smt2 index 99e19e7fb..79fbf2e44 100644 --- a/test/regress/regress2/bug394.smt2 +++ b/test/regress/regress2/bug394.smt2 @@ -13,7 +13,7 @@ ; EXPECT: sat ;(set-option :produce-unsat-cores true) (set-option :print-success false) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) ;(set-option :produce-models true) (set-logic ALL_SUPPORTED) ; done setting options diff --git a/test/regress/regress2/bug812.smt2 b/test/regress/regress2/bug812.smt2 index 8bc87fa52..79eb1c72c 100644 --- a/test/regress/regress2/bug812.smt2 +++ b/test/regress/regress2/bug812.smt2 @@ -3,7 +3,7 @@ VCC and HAVOC benchmarks. Contributed by Nikolaj Bjorner, Leonardo de Moura,
Michal Moskal, and Shaz Qadeer.
|) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun x (Int Int) Int) diff --git a/test/regress/regress2/hash_sat_06_19.smt2 b/test/regress/regress2/hash_sat_06_19.smt2 index b565a4b57..d7f5ff7d4 100644 --- a/test/regress/regress2/hash_sat_06_19.smt2 +++ b/test/regress/regress2/hash_sat_06_19.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIA) (set-info :source | MathSat group |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun hash_1 (Int) Int) diff --git a/test/regress/regress2/hash_sat_07_17.smt2 b/test/regress/regress2/hash_sat_07_17.smt2 index 0bb49801a..73220dd08 100644 --- a/test/regress/regress2/hash_sat_07_17.smt2 +++ b/test/regress/regress2/hash_sat_07_17.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIA) (set-info :source | MathSat group |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun hash_1 (Int) Int) diff --git a/test/regress/regress2/hash_sat_09_09.smt2 b/test/regress/regress2/hash_sat_09_09.smt2 index 6dc26542e..5924973e9 100644 --- a/test/regress/regress2/hash_sat_09_09.smt2 +++ b/test/regress/regress2/hash_sat_09_09.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIA) (set-info :source | MathSat group |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun hash_1 (Int) Int) diff --git a/test/regress/regress2/hash_sat_10_09.smt2 b/test/regress/regress2/hash_sat_10_09.smt2 index 20cff8b1b..0a60ed9b5 100644 --- a/test/regress/regress2/hash_sat_10_09.smt2 +++ b/test/regress/regress2/hash_sat_10_09.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIA) (set-info :source | MathSat group |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun hash_1 (Int) Int) diff --git a/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 b/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 index 9a737a3d1..6daa38e01 100644 --- a/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 +++ b/test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIA) (set-info :source | Simplify Theorem Prover Benchmark Suite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status sat) (declare-fun true_term () Int) diff --git a/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 b/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 index ff7c09997..da9800ca8 100644 --- a/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 +++ b/test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIA) (set-info :source | Simplify Theorem Prover Benchmark Suite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status sat) (declare-fun true_term () Int) diff --git a/test/regress/regress2/nl/nt-lemmas-bad.smt2 b/test/regress/regress2/nl/nt-lemmas-bad.smt2 index cea877c23..43a5f3d88 100644 --- a/test/regress/regress2/nl/nt-lemmas-bad.smt2 +++ b/test/regress/regress2/nl/nt-lemmas-bad.smt2 @@ -18,7 +18,7 @@ Submitted by Dejan Jovanovic for SMT-LIB. |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun skoX () Real) diff --git a/test/regress/regress2/ooo.rf6.smt2 b/test/regress/regress2/ooo.rf6.smt2 index 4860a3428..63cebc50c 100644 --- a/test/regress/regress2/ooo.rf6.smt2 +++ b/test/regress/regress2/ooo.rf6.smt2 @@ -5,7 +5,7 @@ UCLID benchmark suite. See UCLID project: http://www.cs.cmu.edu/~uclid This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun BOOOB_46_init_null_val () Int) diff --git a/test/regress/regress2/ooo.tag10.smt2 b/test/regress/regress2/ooo.tag10.smt2 index ef8e2244c..2d5cb3b37 100644 --- a/test/regress/regress2/ooo.tag10.smt2 +++ b/test/regress/regress2/ooo.tag10.smt2 @@ -5,7 +5,7 @@ UCLID benchmark suite. See UCLID project: http://www.cs.cmu.edu/~uclid This benchmark was automatically translated into SMT-LIB format from CVC format using CVC Lite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun Br1 () Int) diff --git a/test/regress/regress2/piVC_5581bd.smt2 b/test/regress/regress2/piVC_5581bd.smt2 index 78baeea84..aab556d69 100644 --- a/test/regress/regress2/piVC_5581bd.smt2 +++ b/test/regress/regress2/piVC_5581bd.smt2 @@ -1,6 +1,6 @@ (set-logic AUFLIA) (set-info :source |piVC|) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun V_26 () Int) diff --git a/test/regress/regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 b/test/regress/regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 index bbd32d988..a8559a90a 100644 --- a/test/regress/regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 +++ b/test/regress/regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 @@ -3,7 +3,7 @@ Boogie/Spec# benchmarks. This benchmark was translated by Michal Moskal. |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun boolIff (Int Int) Int) diff --git a/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 b/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 index 811796bbf..dcdc41886 100644 --- a/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 +++ b/test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 @@ -1,6 +1,6 @@ (set-logic AUFLIA) (set-info :source | Simplify Theorem Prover Benchmark Suite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun true_term () Int) diff --git a/test/regress/regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 b/test/regress/regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 index fd672bd3b..d608ce067 100644 --- a/test/regress/regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 +++ b/test/regress/regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -1,6 +1,6 @@ (set-logic AUFLIA) (set-info :source | Simplify Theorem Prover Benchmark Suite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun true_term () Int) diff --git a/test/regress/regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 b/test/regress/regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 index 9a5c07194..9a2eb411a 100644 --- a/test/regress/regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 +++ b/test/regress/regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 @@ -1,6 +1,6 @@ (set-logic AUFLIA) (set-info :source | Simplify Theorem Prover Benchmark Suite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun true_term () Int) diff --git a/test/regress/regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 b/test/regress/regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 index e0938975c..f932c5349 100644 --- a/test/regress/regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 +++ b/test/regress/regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 @@ -3,7 +3,7 @@ Simplify front end test suite. This benchmark was translated by Michal Moskal. |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun L_102.5 () Int) diff --git a/test/regress/regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 b/test/regress/regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 index 2867e618f..a08a007c6 100644 --- a/test/regress/regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 +++ b/test/regress/regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 @@ -1,6 +1,6 @@ (set-logic AUFLIA) (set-info :source | Simplify Theorem Prover Benchmark Suite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status unsat) (declare-fun true_term () Int) diff --git a/test/regress/regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 b/test/regress/regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 index 6dc6318a4..4adf5e7cb 100644 --- a/test/regress/regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 +++ b/test/regress/regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIA) (set-info :source | Simplify Theorem Prover Benchmark Suite |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status sat) (declare-fun true_term () Int) diff --git a/test/regress/regress2/strings/cmu-dis-0707-3.smt2 b/test/regress/regress2/strings/cmu-dis-0707-3.smt2 index 3bf47ed61..fcdcded39 100644 --- a/test/regress/regress2/strings/cmu-dis-0707-3.smt2 +++ b/test/regress/regress2/strings/cmu-dis-0707-3.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --lang=smt2.0 ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) +(set-info :smt-lib-version 2.6) (set-option :strings-exp true) (declare-fun value () String) (declare-fun name () String) @@ -11,12 +11,12 @@ (assert (not (not (= (ite (> (str.indexof value ":" 0) 0) 1 0) 0)))) (assert (not (= (ite (not (= (str.len value) 0)) 1 0) 0))) (assert (not (not (= (ite (str.contains value "'") 1 0) 0)))) -(assert (not (not (= (ite (str.contains value "\"") 1 0) 0)))) +(assert (not (not (= (ite (str.contains value "\\""") 1 0) 0)))) (assert (not (not (= (ite (str.contains value ">") 1 0) 0)))) (assert (not (not (= (ite (str.contains value "<") 1 0) 0)))) (assert (not (not (= (ite (str.contains value "&") 1 0) 0)))) (assert (not (not (= (ite (str.contains name "'") 1 0) 0)))) -(assert (not (not (= (ite (str.contains name "\"") 1 0) 0)))) +(assert (not (not (= (ite (str.contains name "\\""") 1 0) 0)))) (assert (not (not (= (ite (str.contains name ">") 1 0) 0)))) (assert (not (not (= (ite (str.contains name "<") 1 0) 0)))) (assert (not (not (= (ite (str.contains name "&") 1 0) 0)))) diff --git a/test/regress/regress2/strings/issue918.smt2 b/test/regress/regress2/strings/issue918.smt2 index 0843a1700..c335ca642 100644 --- a/test/regress/regress2/strings/issue918.smt2 +++ b/test/regress/regress2/strings/issue918.smt2 @@ -1,12 +1,9 @@ ; COMMAND-LINE: --strings-exp --re-elim ; EXPECT: sat -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-option :produce-models true) (set-logic UFDTSLIA) -(declare-datatypes () ( - (StringRotation (StringRotation$C_StringRotation (StringRotation$C_StringRotation$sr String))) - (StringRotation2 (StringRotation2$C_StringRotation2 (StringRotation2$C_StringRotation2$sr1 StringRotation) (StringRotation2$C_StringRotation2$sr2 StringRotation))) -) ) +(declare-datatypes ((StringRotation 0)(StringRotation2 0)) (((StringRotation$C_StringRotation (StringRotation$C_StringRotation$sr String)))((StringRotation2$C_StringRotation2 (StringRotation2$C_StringRotation2$sr1 StringRotation) (StringRotation2$C_StringRotation2$sr2 StringRotation))))) (define-fun f1005$isValid_string((x$$1008 String)) Bool true) (define-fun f1035$isValid_StringRotation((x$$1038 StringRotation)) Bool (and (f1005$isValid_string (StringRotation$C_StringRotation$sr x$$1038)) (or (or (or (= (StringRotation$C_StringRotation$sr x$$1038) "0 deg") (= (StringRotation$C_StringRotation$sr x$$1038) "90 deg")) (= (StringRotation$C_StringRotation$sr x$$1038) "180 deg")) (= (StringRotation$C_StringRotation$sr x$$1038) "270 deg")))) @@ -14,17 +11,7 @@ (declare-fun $OutSR$1356$3$1$() StringRotation2) (assert (f1121$isValid_StringRotation2 $OutSR$1356$3$1$)) -(assert (and (is-StringRotation2$C_StringRotation2 $OutSR$1356$3$1$) (and (and -(is-StringRotation$C_StringRotation (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$)) (or -(str.in.re -(StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$)) -(re.++ (re.union (re.range "u" "~") (re.range " " "t") ) (re.union (re.range "K" "~") (re.range " " "J") ) (re.union (re.range "L" "~") (re.range " " "K") ) (re.union (re.range "y" "~") (re.range " " "x") ) (re.union (re.range "{" "~") (re.range " " "z") ) ) -) -(or -(str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$)) -(re.++ (re.union (re.range "s" "~") (re.range " " "r") ) (re.union (re.range "{" "~") (re.range " " "z") ) (re.union (re.range "u" "~") (re.range " " "t") ) ) ) +(assert (let ((_let_1 (re.* (re.union (re.range "\u{0}" "\u{9}") (re.range "\u{b}" "\u{c}") (re.range "\u{e}" "\u{7f}"))))) (let ((_let_2 (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$))) (let ((_let_3 (StringRotation$C_StringRotation$sr _let_2))) (let ((_let_4 (re.union (re.range "n" "~") (re.range " " "m")))) (let ((_let_5 (re.union (re.range "u" "~") (re.range " " "t")))) (let ((_let_6 (re.union (re.range "<" "~") (re.range " " ";")))) (let ((_let_7 (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$))) (let ((_let_8 (StringRotation$C_StringRotation$sr _let_7))) (let ((_let_9 (re.union (re.range "s" "~") (re.range " " "r")))) (let ((_let_10 (re.union (re.range "{" "~") (re.range " " "z")))) (and ((_ is StringRotation2$C_StringRotation2) $OutSR$1356$3$1$) (and (and ((_ is StringRotation$C_StringRotation) _let_7) (or (str.in_re _let_8 (re.++ _let_5 (re.union (re.range "K" "~") (re.range " " "J")) (re.union (re.range "L" "~") (re.range " " "K")) (re.union (re.range "y" "~") (re.range " " "x")) _let_10)) (or (str.in_re _let_8 (re.++ _let_9 _let_10 _let_5)) (or (str.in_re _let_8 _let_6) (or (str.in_re _let_8 (re.++ (re.union (re.range "&" "~") (re.range " " "%")) (re.range " " "~"))) (or (str.in_re _let_8 (re.++ (re.union (re.range "`" "~") (re.range " " "_")) _let_9 (re.union (re.range "1" "~") (re.range " " "0")) (re.union (re.range "_" "~") (re.range " " "^")))) (str.in_re _let_8 _let_1))))))) (and ((_ is StringRotation$C_StringRotation) _let_2) (or (str.in_re _let_3 (re.++ _let_6 (re.union (re.range "F" "~") (re.range " " "E")) _let_5 (re.union (re.range "P" "~") (re.range " " "O")))) (or (str.in_re _let_3 (re.union (re.range "E" "~") (re.range " " "D"))) (or (str.in_re _let_3 (re.++ (re.union (re.range "x" "~") (re.range " " "w")) _let_4 (re.union (re.range "d" "~") (re.range " " "c")) (re.union (re.range "]" "~") (re.range " " "\u{5c}")) (re.union (re.range "\u{5c}" "~") (re.range " " "[")))) (or (str.in_re _let_3 (re.++ (re.union (re.range ":" "~") (re.range " " "9")) (re.union (re.range "+" "~") (re.range " " "*")))) (or (str.in_re _let_3 (re.++ (re.union (re.range "." "~") (re.range " " "-")) _let_4 (re.union (re.range "|" "~") (re.range " " "{")))) (str.in_re _let_3 _let_1)))))))))))))))))))) -(or -(str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$)) (re.union (re.range "<" "~") (re.range " " ";") ) ) (or (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$)) (re.++ (re.union (re.range "&" "~") (re.range " " "%") ) (re.range " " "~") ) ) (or (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$)) (re.++ (re.union (re.range "`" "~") (re.range " " "_") ) (re.union (re.range "s" "~") (re.range " " "r") ) (re.union (re.range "1" "~") (re.range " " "0") ) (re.union (re.range "_" "~") (re.range " " "^") ) ) ) (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr1 $OutSR$1356$3$1$)) (re.* (re.union (re.range "\x00" "\x09") (re.range "\x0B" "\x0C") (re.range "\x0E" "\x7F") ) ) ))))))) (and (is-StringRotation$C_StringRotation (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$)) (or (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$)) (re.++ (re.union (re.range "<" "~") (re.range " " ";") ) (re.union (re.range "F" "~") (re.range " " "E") ) (re.union (re.range "u" "~") (re.range " " "t") ) (re.union (re.range "P" "~") (re.range " " "O") ) ) ) (or (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$)) (re.union (re.range "E" "~") (re.range " " "D") ) ) (or (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$)) (re.++ (re.union (re.range "x" "~") (re.range " " "w") ) (re.union (re.range "n" "~") (re.range " " "m") ) (re.union (re.range "d" "~") (re.range " " "c") ) (re.union (re.range "]" "~") (re.range " " "\\") ) (re.union (re.range "\\" "~") (re.range " " "[") ) ) ) (or (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$)) (re.++ (re.union (re.range ":" "~") (re.range " " "9") ) (re.union (re.range "+" "~") (re.range " " "*") ) ) ) (or (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$)) (re.++ (re.union (re.range "." "~") (re.range " " "-") ) (re.union (re.range "n" "~") (re.range " " "m") ) (re.union (re.range "|" "~") (re.range " " "{") ) ) ) (str.in.re (StringRotation$C_StringRotation$sr (StringRotation2$C_StringRotation2$sr2 $OutSR$1356$3$1$)) (re.* (re.union (re.range "\x00" "\x09") (re.range "\x0B" "\x0C") (re.range "\x0E" "\x7F") ) ) )))))))))) (check-sat) |