Remove SMT-LIB 2.5 and 2.0 support. (#6068)

This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.

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)