Fixes some initialization and desctruction problems in quantifiers. Also restricts...

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 9e13ef5eb82ae091086ef2e1ecea10f5766c230b..cd304c6d420a127fd2f59e7c577e3114dfc98b12 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -770,7 +770,28 @@ void QuantInfo::debugPrintMatch( const char * c ) {
   }
 }
 
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
+MatchGen::MatchGen()
+  : d_matched_basis(),
+    d_binding(),
+    d_tgt(),
+    d_tgt_orig(),
+    d_wasSet(),
+    d_n(),
+    d_type( typ_invalid ),
+    d_type_not()
+{}
+
+
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
+  : d_matched_basis(),
+    d_binding(),
+    d_tgt(),
+    d_tgt_orig(),
+    d_wasSet(),
+    d_n(),
+    d_type(),
+    d_type_not()
+{
   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
   std::vector< Node > qni_apps;
   d_qni_size = 0;

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index d2a9827817a9d48bc66afb9df1a4c7a96986c3e9..11299b532d1a4b8eb78999cdd82b9f42aac543b6 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -78,7 +78,7 @@ public:
   };
   void debugPrintType( const char * c, short typ, bool isTrace = false );
 public:
-  MatchGen() : d_type( typ_invalid ){}
+  MatchGen();
   MatchGen( QuantInfo * qi, Node n, bool isVar = false );
   bool d_tgt;
   bool d_tgt_orig;

diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index 0de6341cbe083409a050eab34c9c951dcc3b0171..35a328147654ea4ef044cdc2ca57bc938ca9a701 100755 (executable)
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -64,7 +64,7 @@ private:
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 public:
   QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
-  ~QuantEqualityEngine(){}
+  virtual ~QuantEqualityEngine() throw (){}
 
   /* whether this module needs to check this round */
   bool needsCheck( Theory::Effort e );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9ae3b1d40795b4e828807cdc6e038069cab61f60..cfe53dd0f958413793f4bbc9ecabea3150c474fd 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -229,6 +229,7 @@ d_presolve_cache_wic(u){
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
+  delete d_alpha_equiv;
   delete d_builder;
   delete d_rr_engine;
   delete d_bint;

diff --git a/test/regress/regress0/bug605.cvc b/test/regress/regress0/bug605.cvc
index 1ccf7fa9e102b31ca678102f2a2bf5544f950b2d..56446493161031474e40c75f196aee2536582ba5 100644 (file)
--- a/test/regress/regress0/bug605.cvc
+++ b/test/regress/regress0/bug605.cvc
@@ -1,30 +1,30 @@
-% EXPECT: sat\r
-OPTION "produce-models";\r
-\r
-% GeoLocation\r
-GeoLocation: TYPE = [# longitude: INT, latitude: INT #];\r
-\r
-% Stationary object\r
-StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];\r
-Facet: TYPE = [# base: StationaryObject #];\r
-\r
-Segment: TYPE = [# s_f: Facet #];\r
-A : TYPE = ARRAY INT OF Segment;\r
-a : A;\r
-\r
-p1: GeoLocation = (# longitude := 0, latitude := 0 #);\r
-\r
-s1: StationaryObject = (# geoLoc := {p1} #);\r
-\r
-\r
-f0: Facet = (# base := s1 #);\r
-\r
-\r
-init: (A, INT, Facet) -> BOOLEAN\r
-  = LAMBDA (v: A, i: INT, f: Facet): \r
-    v[0].s_f = f;\r
-    \r
-    \r
-ASSERT (init(a, 2, f0));\r
-\r
-CHECKSAT TRUE;\r
+% EXPECT: sat
+OPTION "produce-models";
+
+% GeoLocation
+GeoLocation: TYPE = [# longitude: INT, latitude: INT #];
+
+% Stationary object
+StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];
+Facet: TYPE = [# base: StationaryObject #];
+
+Segment: TYPE = [# s_f: Facet #];
+A : TYPE = ARRAY INT OF Segment;
+a : A;
+
+p1: GeoLocation = (# longitude := 0, latitude := 0 #);
+
+s1: StationaryObject = (# geoLoc := {p1} #);
+
+
+f0: Facet = (# base := s1 #);
+
+
+init: (A, INT, Facet) -> BOOLEAN
+  = LAMBDA (v: A, i: INT, f: Facet): 
+    v[0].s_f = f;
+    
+    
+ASSERT (init(a, 2, f0));
+
+CHECKSAT TRUE;

diff --git a/test/regress/regress0/datatypes/cdt-model-cade15.smt2 b/test/regress/regress0/datatypes/cdt-model-cade15.smt2
index 5b570a915eca74ee011fc2b5f6d896393cde8bb3..c23a9d594af88837f1c4c50e5161cd7fcf24e46a 100755 (executable)
--- a/test/regress/regress0/datatypes/cdt-model-cade15.smt2
+++ b/test/regress/regress0/datatypes/cdt-model-cade15.smt2
@@ -1,17 +1,17 @@
-(set-logic ALL_SUPPORTED)\r
-(set-info :status sat)\r
-(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream)))))\r
-\r
-(declare-const z Stream)\r
-(declare-const x Stream)\r
-(declare-const y Stream)\r
-(declare-const u Stream)\r
-(declare-const v Stream)\r
-(declare-const w Stream)\r
-\r
-(assert (= u (C z)))\r
-(assert (= v (D z)))\r
-(assert (= w (E y)))\r
-(assert (= x (C v)))\r
-(assert (distinct x y z u v w))\r
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream)))))
+
+(declare-const z Stream)
+(declare-const x Stream)
+(declare-const y Stream)
+(declare-const u Stream)
+(declare-const v Stream)
+(declare-const w Stream)
+
+(assert (= u (C z)))
+(assert (= v (D z)))
+(assert (= w (E y)))
+(assert (= x (C v)))
+(assert (distinct x y z u v w))
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/quantifiers/floor.smt2 b/test/regress/regress0/quantifiers/floor.smt2
index cb20c1056acc22da6856e26cb92e6849973168d3..47aea95bfea9bb41120f4e3fc2d45c7a9f04a9d4 100755 (executable)
--- a/test/regress/regress0/quantifiers/floor.smt2
+++ b/test/regress/regress0/quantifiers/floor.smt2
@@ -1,4 +1,4 @@
-(set-logic LIRA)\r
-(set-info :status unsat)\r
-(assert (forall ((X Real)) (not (>= (+ (to_int (* 2 X)) (* (- 2) (to_int X))) 1)) ))\r
+(set-logic LIRA)
+(set-info :status unsat)
+(assert (forall ((X Real)) (not (>= (+ (to_int (* 2 X)) (* (- 2) (to_int X))) 1)) ))
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/quantifiers/is-int.smt2 b/test/regress/regress0/quantifiers/is-int.smt2
index 07e8dd2463c9b8c7e4d21d735d47e45dc428ef5b..fc7fbb180dd0e5dbf350d23fa0b2db85a0ced489 100755 (executable)
--- a/test/regress/regress0/quantifiers/is-int.smt2
+++ b/test/regress/regress0/quantifiers/is-int.smt2
@@ -1,4 +1,4 @@
-(set-logic LIRA)\r
-(set-info :status unsat)\r
-(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) ))\r
+(set-logic LIRA)
+(set-info :status unsat)
+(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) ))
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/bug686dd.smt2 b/test/regress/regress0/strings/bug686dd.smt2
index 7db4b86f07f5b8b2c2b3b487d7eb1779aca38e6a..688cecec15d540310718d04ae614b394b6379c77 100644 (file)
--- a/test/regress/regress0/strings/bug686dd.smt2
+++ b/test/regress/regress0/strings/bug686dd.smt2
@@ -1,13 +1,13 @@
-(set-logic UFDTSLIA)\r
-(set-info :status sat)\r
-\r
-(declare-datatypes () ( (T (TC (TCb String))) ) )\r
-\r
-(declare-fun root5 () String)\r
-(declare-fun root6 () T)\r
-\r
-(assert (and \r
-(str.in.re root5 (re.loop (re.range "0" "9") 4 4) )\r
-(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) )\r
-) )\r
-(check-sat)\r
+(set-logic UFDTSLIA)
+(set-info :status sat)
+
+(declare-datatypes () ( (T (TC (TCb String))) ) )
+
+(declare-fun root5 () String)
+(declare-fun root6 () T)
+
+(assert (and 
+(str.in.re root5 (re.loop (re.range "0" "9") 4 4) )
+(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) )
+) )
+(check-sat)

diff --git a/test/regress/regress0/strings/chapman150408.smt2 b/test/regress/regress0/strings/chapman150408.smt2
index 546c46e322b5c7d2e4f31dc63d89574012d18a43..f037185565f806e5afa3999a19a1d9676d998f7d 100644 (file)
--- a/test/regress/regress0/strings/chapman150408.smt2
+++ b/test/regress/regress0/strings/chapman150408.smt2
@@ -1,10 +1,10 @@
-(set-logic SLIA)\r
-(set-info :status sat)\r
-(set-option :strings-exp true)\r
-(set-option :rewrite-divk true)\r
-(declare-fun string () String)\r
-(assert (and\r
-     (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0)\r
-     0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not\r
-     (not (= (ite (str.contains string "]") 1 0) 0)))))\r
-(check-sat)\r
+(set-logic SLIA)
+(set-info :status sat)
+(set-option :strings-exp true)
+(set-option :rewrite-divk true)
+(declare-fun string () String)
+(assert (and
+     (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0)
+     0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not
+     (not (= (ite (str.contains string "]") 1 0) 0)))))
+(check-sat)

diff --git a/test/regress/regress0/strings/crash-1019.smt2 b/test/regress/regress0/strings/crash-1019.smt2
index 1a41ba7152cbf75b750ae0c8061d3f6c795813dd..9f2e99b02ae8f988c2616395d55abdf32d9e0002 100755 (executable)
--- a/test/regress/regress0/strings/crash-1019.smt2
+++ b/test/regress/regress0/strings/crash-1019.smt2
@@ -1,10 +1,10 @@
-(set-logic ALL_SUPPORTED)\r
-(set-option :strings-exp true)\r
-(set-option :rewrite-divk true)\r
-(set-info :status unsat)\r
- \r
-(declare-fun s () String)\r
- \r
-(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))))\r
- \r
-(check-sat)\r
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-option :rewrite-divk true)
+(set-info :status unsat)
+ 
+(declare-fun s () String)
+ 
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))))
+ 
+(check-sat)

diff --git a/test/regress/regress0/strings/ilc-l-nt.smt2 b/test/regress/regress0/strings/ilc-l-nt.smt2
index 32dfc0b1bde7b65c760150d8d0510a81524e6345..9e1cc2bc592f91f4bc1b721c86035b177c8dd1e2 100755 (executable)
--- a/test/regress/regress0/strings/ilc-l-nt.smt2
+++ b/test/regress/regress0/strings/ilc-l-nt.smt2
@@ -1,14 +1,14 @@
-(set-logic ALL_SUPPORTED)\r
-(set-info :status unsat)\r
-(set-option :strings-exp true)\r
- \r
-(declare-fun s () String)\r
-(assert (or (= s "Id like cookies.") (= s "Id not like cookies.")))\r
- \r
-(declare-fun target () String)\r
-(assert (or (= target "l") (= target "m")))\r
- \r
-(declare-fun location () Int)\r
-(assert (= (* 2 location) (str.indexof s target 0)))\r
- \r
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+ 
+(declare-fun s () String)
+(assert (or (= s "Id like cookies.") (= s "Id not like cookies.")))
+ 
+(declare-fun target () String)
+(assert (or (= target "l") (= target "m")))
+ 
+(declare-fun location () Int)
+(assert (= (* 2 location) (str.indexof s target 0)))
+ 
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/ilc-like.smt2 b/test/regress/regress0/strings/ilc-like.smt2
index a711c215c133d5cfcb5d20dd246b2c70e20cb815..bb708ee5cb6cbce9a9a2f99cfbf8596057ab03e5 100755 (executable)
--- a/test/regress/regress0/strings/ilc-like.smt2
+++ b/test/regress/regress0/strings/ilc-like.smt2
@@ -1,14 +1,14 @@
-(set-logic ALL_SUPPORTED)\r
-(set-info :status sat)\r
-(set-option :strings-exp true)\r
- \r
-(declare-fun s () String)\r
-(assert (= s "I like cookies."))\r
- \r
-(declare-fun target () String)\r
-(assert (= target "like"))\r
- \r
-(declare-fun location () Int)\r
-(assert (= location (str.indexof s target 0)))\r
- \r
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+ 
+(declare-fun s () String)
+(assert (= s "I like cookies."))
+ 
+(declare-fun target () String)
+(assert (= target "like"))
+ 
+(declare-fun location () Int)
+(assert (= location (str.indexof s target 0)))
+ 
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/indexof-sym-simp.smt2 b/test/regress/regress0/strings/indexof-sym-simp.smt2
index 7ae60f2db11df24302147265c4ed6446d19aec45..f4cf5c0555baf8aaea2696babf9029c9653319a3 100755 (executable)
--- a/test/regress/regress0/strings/indexof-sym-simp.smt2
+++ b/test/regress/regress0/strings/indexof-sym-simp.smt2
@@ -1,10 +1,10 @@
-(set-logic ALL_SUPPORTED)\r
-(set-info :status unsat)\r
-(set-option :strings-exp true)\r
-(declare-fun s () String)\r
-(declare-fun t () String)\r
-(declare-fun r () String)\r
-; solvable if we do equality reasoning over str.indexof\r
-(assert (= t s))\r
-(assert (not (= (str.indexof t r 0) (str.indexof s r 0))))\r
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+(declare-fun s () String)
+(declare-fun t () String)
+(declare-fun r () String)
+; solvable if we do equality reasoning over str.indexof
+(assert (= t s))
+(assert (not (= (str.indexof t r 0) (str.indexof s r 0))))
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/kaluza-fl.smt2 b/test/regress/regress0/strings/kaluza-fl.smt2
index ce3af9e74b522d30d8c4dc52832a0ad8eaaaa015..04775d61c7ea95360f8f82758ea470562756e853 100755 (executable)
--- a/test/regress/regress0/strings/kaluza-fl.smt2
+++ b/test/regress/regress0/strings/kaluza-fl.smt2
@@ -1,97 +1,97 @@
-(set-logic QF_S)\r
-(set-info :status sat)\r
-\r
-(declare-fun I0_15 () Int)\r
-(declare-fun I0_18 () Int)\r
-(declare-fun I0_2 () Int)\r
-(declare-fun I0_4 () Int)\r
-(declare-fun I0_6 () Int)\r
-(declare-fun PCTEMP_LHS_1 () Int)\r
-(declare-fun PCTEMP_LHS_2 () Int)\r
-(declare-fun PCTEMP_LHS_3 () Int)\r
-(declare-fun PCTEMP_LHS_4 () Int)\r
-(declare-fun PCTEMP_LHS_5 () Int)\r
-(declare-fun T0_15 () String)\r
-(declare-fun T0_18 () String)\r
-(declare-fun T0_2 () String)\r
-(declare-fun T0_4 () String)\r
-(declare-fun T0_6 () String)\r
-(declare-fun T1_15 () String)\r
-(declare-fun T1_18 () String)\r
-(declare-fun T1_2 () String)\r
-(declare-fun T1_4 () String)\r
-(declare-fun T1_6 () String)\r
-(declare-fun T2_15 () String)\r
-(declare-fun T2_18 () String)\r
-(declare-fun T2_2 () String)\r
-(declare-fun T2_4 () String)\r
-(declare-fun T2_6 () String)\r
-(declare-fun T3_15 () String)\r
-(declare-fun T3_18 () String)\r
-(declare-fun T3_2 () String)\r
-(declare-fun T3_4 () String)\r
-(declare-fun T3_6 () String)\r
-(declare-fun T4_15 () String)\r
-(declare-fun T4_18 () String)\r
-(declare-fun T4_2 () String)\r
-(declare-fun T4_4 () String)\r
-(declare-fun T4_6 () String)\r
-(declare-fun T5_15 () String)\r
-(declare-fun T5_18 () String)\r
-(declare-fun T5_2 () String)\r
-(declare-fun T5_4 () String)\r
-(declare-fun T5_6 () String)\r
-(declare-fun T_4 () Bool)\r
-(declare-fun T_5 () Bool)\r
-(declare-fun T_6 () Bool)\r
-(declare-fun T_7 () Bool)\r
-(declare-fun T_8 () Bool)\r
-(declare-fun T_9 () Bool)\r
-(declare-fun T_SELECT_1 () Bool)\r
-(declare-fun T_SELECT_2 () Bool)\r
-(declare-fun T_SELECT_3 () Bool)\r
-(declare-fun T_SELECT_4 () Bool)\r
-(declare-fun T_SELECT_5 () Bool)\r
-(declare-fun T_a () Bool)\r
-(declare-fun T_c () Bool)\r
-(declare-fun T_e () Bool)\r
-(declare-fun var_0xINPUT_12454 () String)\r
-\r
-(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))\r
-(assert (ite T_SELECT_1 \r
-  (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))) \r
-  (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re ".")))))))\r
-(assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1)))))\r
-(assert (ite T_SELECT_2 \r
-  (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) \r
-  (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))\r
-(assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1)))))\r
-(assert (ite T_SELECT_3 \r
-  (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) \r
-  (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))\r
-(assert (= T_4 (<= 0 PCTEMP_LHS_1)))\r
-(assert T_4)\r
-(assert (= T_5 (<= 0 PCTEMP_LHS_2)))\r
-(assert T_5)\r
-(assert (= T_6 (<= 0 PCTEMP_LHS_3)))\r
-(assert T_6)\r
-(assert (= T_7 (= "" var_0xINPUT_12454)))\r
-(assert (= T_8 (not T_7)))\r
-(assert T_8)\r
-(assert (= T_9 (= var_0xINPUT_12454 "")))\r
-(assert (= T_a (not T_9)))\r
-(assert T_a)\r
-(assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1)))))\r
-(assert (ite T_SELECT_4 \r
-  (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) \r
-  (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))\r
-(assert (= T_c (< (- 1) PCTEMP_LHS_4)))\r
-(assert T_c)\r
-(assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1)))))\r
-(assert (ite T_SELECT_5 \r
-  (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";")))) \r
-  (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";"))))))\r
-(assert (= T_e (< PCTEMP_LHS_5 0)))\r
-(assert T_e)\r
-\r
-(check-sat)\r
+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun I0_15 () Int)
+(declare-fun I0_18 () Int)
+(declare-fun I0_2 () Int)
+(declare-fun I0_4 () Int)
+(declare-fun I0_6 () Int)
+(declare-fun PCTEMP_LHS_1 () Int)
+(declare-fun PCTEMP_LHS_2 () Int)
+(declare-fun PCTEMP_LHS_3 () Int)
+(declare-fun PCTEMP_LHS_4 () Int)
+(declare-fun PCTEMP_LHS_5 () Int)
+(declare-fun T0_15 () String)
+(declare-fun T0_18 () String)
+(declare-fun T0_2 () String)
+(declare-fun T0_4 () String)
+(declare-fun T0_6 () String)
+(declare-fun T1_15 () String)
+(declare-fun T1_18 () String)
+(declare-fun T1_2 () String)
+(declare-fun T1_4 () String)
+(declare-fun T1_6 () String)
+(declare-fun T2_15 () String)
+(declare-fun T2_18 () String)
+(declare-fun T2_2 () String)
+(declare-fun T2_4 () String)
+(declare-fun T2_6 () String)
+(declare-fun T3_15 () String)
+(declare-fun T3_18 () String)
+(declare-fun T3_2 () String)
+(declare-fun T3_4 () String)
+(declare-fun T3_6 () String)
+(declare-fun T4_15 () String)
+(declare-fun T4_18 () String)
+(declare-fun T4_2 () String)
+(declare-fun T4_4 () String)
+(declare-fun T4_6 () String)
+(declare-fun T5_15 () String)
+(declare-fun T5_18 () String)
+(declare-fun T5_2 () String)
+(declare-fun T5_4 () String)
+(declare-fun T5_6 () String)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun T_6 () Bool)
+(declare-fun T_7 () Bool)
+(declare-fun T_8 () Bool)
+(declare-fun T_9 () Bool)
+(declare-fun T_SELECT_1 () Bool)
+(declare-fun T_SELECT_2 () Bool)
+(declare-fun T_SELECT_3 () Bool)
+(declare-fun T_SELECT_4 () Bool)
+(declare-fun T_SELECT_5 () Bool)
+(declare-fun T_a () Bool)
+(declare-fun T_c () Bool)
+(declare-fun T_e () Bool)
+(declare-fun var_0xINPUT_12454 () String)
+
+(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))
+(assert (ite T_SELECT_1 
+  (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))) 
+  (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re ".")))))))
+(assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1)))))
+(assert (ite T_SELECT_2 
+  (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
+  (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1)))))
+(assert (ite T_SELECT_3 
+  (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
+  (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_4 (<= 0 PCTEMP_LHS_1)))
+(assert T_4)
+(assert (= T_5 (<= 0 PCTEMP_LHS_2)))
+(assert T_5)
+(assert (= T_6 (<= 0 PCTEMP_LHS_3)))
+(assert T_6)
+(assert (= T_7 (= "" var_0xINPUT_12454)))
+(assert (= T_8 (not T_7)))
+(assert T_8)
+(assert (= T_9 (= var_0xINPUT_12454 "")))
+(assert (= T_a (not T_9)))
+(assert T_a)
+(assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1)))))
+(assert (ite T_SELECT_4 
+  (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
+  (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_c (< (- 1) PCTEMP_LHS_4)))
+(assert T_c)
+(assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1)))))
+(assert (ite T_SELECT_5 
+  (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";")))) 
+  (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";"))))))
+(assert (= T_e (< PCTEMP_LHS_5 0)))
+(assert T_e)
+
+(check-sat)

diff --git a/test/regress/regress0/strings/norn-ab.smt2 b/test/regress/regress0/strings/norn-ab.smt2
index db7aac7329f333944285cfcf5abb87246fffef78..48d88984713dd587faf417882893fcf48ed7aafc 100755 (executable)
--- a/test/regress/regress0/strings/norn-ab.smt2
+++ b/test/regress/regress0/strings/norn-ab.smt2
@@ -1,25 +1,25 @@
-(set-logic QF_SLIA)\r
-(set-info :status unsat)\r
-(set-option :strings-exp true)\r
-\r
-(declare-fun var_0 () String)\r
-(declare-fun var_1 () String)\r
-(declare-fun var_2 () String)\r
-(declare-fun var_3 () String)\r
-(declare-fun var_4 () String)\r
-(declare-fun var_5 () String)\r
-(declare-fun var_6 () String)\r
-(declare-fun var_7 () String)\r
-(declare-fun var_8 () String)\r
-(declare-fun var_9 () String)\r
-(declare-fun var_10 () String)\r
-(declare-fun var_11 () String)\r
-(declare-fun var_12 () String)\r
-\r
-(assert (str.in.re var_4 (re.++ (str.to.re "a") (re.* (str.to.re "b")))))\r
-(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))\r
-(assert (str.in.re var_4 (re.* (re.range "a" "u"))))\r
-(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))\r
-(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")))))))\r
-(assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))\r
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(declare-fun var_11 () String)
+(declare-fun var_12 () String)
+
+(assert (str.in.re var_4 (re.++ (str.to.re "a") (re.* (str.to.re "b")))))
+(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))
+(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
+(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

diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2
index d0cd69cb0368430a0604da7879e5462de80570c8..45f7ede9477e7bb4ecb94477c2b0464ce56be03d 100755 (executable)
--- a/test/regress/regress0/strings/norn-simp-rew.smt2
+++ b/test/regress/regress0/strings/norn-simp-rew.smt2
@@ -1,29 +1,29 @@
-(set-logic QF_SLIA)\r
-(set-option :strings-exp true)\r
-(set-info :status unsat)\r
-\r
-(declare-fun var_0 () String)\r
-(declare-fun var_1 () String)\r
-(declare-fun var_2 () String)\r
-(declare-fun var_3 () String)\r
-(declare-fun var_4 () String)\r
-(declare-fun var_5 () String)\r
-(declare-fun var_6 () String)\r
-(declare-fun var_7 () String)\r
-(declare-fun var_8 () String)\r
-(declare-fun var_9 () String)\r
-(declare-fun var_10 () String)\r
-(declare-fun var_11 () String)\r
-(declare-fun var_12 () String)\r
-\r
-(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"))))))\r
-(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")))))))\r
-(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")))))))\r
-(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")))))\r
-(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"))))))\r
-(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"))))\r
-(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u"))))\r
-(assert (str.in.re var_8 (re.* (re.range "a" "u"))))\r
-(assert (str.in.re var_7 (re.* (re.range "a" "u"))))\r
-(assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))\r
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status unsat)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(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")))))
 (check-sat)
\ No newline at end of file

diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2
index cbaf5f5e4183f187732577edc3db1aefdcb3949b..2b25e6dc8d842aca5205af0bb04088e89bb68ab6 100755 (executable)
--- a/test/regress/regress0/strings/unsound-0908.smt2
+++ b/test/regress/regress0/strings/unsound-0908.smt2
@@ -1,12 +1,12 @@
-(set-logic QF_S)\r
-(set-info :status sat)\r
-(declare-const x String)\r
-(assert (= (str.len x) 1))\r
-;(assert (= x "X"))\r
-(assert\r
-    (or \r
-      (not (> (str.len x) 1))\r
-      (= (str.at x 1) "Z")\r
-    )\r
-)\r
-(check-sat)\r
+(set-logic QF_S)
+(set-info :status sat)
+(declare-const x String)
+(assert (= (str.len x) 1))
+;(assert (= x "X"))
+(assert
+    (or 
+      (not (> (str.len x) 1))
+      (= (str.at x 1) "Z")
+    )
+)
+(check-sat)

diff --git a/test/regress/regress0/uf/cnf-and-neg.smt2 b/test/regress/regress0/uf/cnf-and-neg.smt2
index 711740f6752a896a51fe530b84e018bac726d206..470a88809ddc77012b7ed1f1fc5eba1e941f6ad1 100755 (executable)
--- a/test/regress/regress0/uf/cnf-and-neg.smt2
+++ b/test/regress/regress0/uf/cnf-and-neg.smt2
@@ -1,11 +1,11 @@
-(set-logic QF_UF)\r
-(set-info :status unsat)\r
-(declare-sort I 0)\r
-(declare-fun a () I)\r
-(declare-fun b () I)\r
-(declare-fun c () I)\r
-(declare-fun f (I) I)\r
-(assert (not (= (f a) (f b))))\r
-(assert (not (= (f a) (f c))))\r
-(assert (not (and (not (= a b)) (not (= a c)))))\r
-(check-sat)\r
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort I 0)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+(declare-fun f (I) I)
+(assert (not (= (f a) (f b))))
+(assert (not (= (f a) (f c))))
+(assert (not (and (not (= a b)) (not (= a c)))))
+(check-sat)

diff --git a/test/regress/regress0/uf/cnf_abc.smt2 b/test/regress/regress0/uf/cnf_abc.smt2
index 5d011f44c16bee24107836a929201e7a62ceca5c..46a4b7dbfaf773aa767fb186892529323bdf386f 100755 (executable)
--- a/test/regress/regress0/uf/cnf_abc.smt2
+++ b/test/regress/regress0/uf/cnf_abc.smt2
@@ -1,168 +1,168 @@
-(set-logic QF_UF)\r
-(set-info :status unsat)\r
-\r
-(declare-sort I 0)\r
-(declare-fun f (I I) I)\r
-(declare-fun a () I)\r
-(declare-fun b () I)\r
-(declare-fun c () I)\r
-\r
-\r
-\r
-(assert\r
- (or\r
-  (= (f a a) a)\r
-  (= (f a a) b)\r
-  (= (f a a) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f a b) a)\r
-  (= (f a b) b)\r
-  (= (f a b) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f a c) a)\r
-  (= (f a c) b)\r
-  (= (f a c) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f b a) a)\r
-  (= (f b a) b)\r
-  (= (f b a) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f b b) a)\r
-  (= (f b b) b)\r
-  (= (f b b) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f b c) a)\r
-  (= (f b c) b)\r
-  (= (f b c) c)\r
-  ))\r
-\r
-\r
-(assert\r
- (or\r
-  (= (f c a) a)\r
-  (= (f c a) b)\r
-  (= (f c a) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f c b) a)\r
-  (= (f c b) b)\r
-  (= (f c b) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f c c) a)\r
-  (= (f c c) b)\r
-  (= (f c c) c)\r
-  ))\r
-\r
-\r
-\r
-(assert\r
- (or\r
-  (= (f a a) a)\r
-  (= (f b b) a)\r
-  (= (f c c) a)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f a a) b)\r
-  (= (f b b) b)\r
-  (= (f c c) b)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f a a) c)\r
-  (= (f b b) c)\r
-  (= (f c c) c)\r
-  ))\r
-\r
-\r
-\r
-(assert\r
- (or\r
-  (= (f a a) a)\r
-  (= (f b a) b)\r
-  (= (f c a) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f a b) a)\r
-  (= (f b b) b)\r
-  (= (f c b) c)\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (= (f a c) a)\r
-  (= (f b c) b)\r
-  (= (f c c) c)\r
-  ))\r
-\r
-\r
-\r
-\r
-(assert (not (= (f a a) a)))\r
-(assert (not (= (f b b) b)))\r
-(assert (not (= (f c c) c)))                \r
-\r
-\r
-(assert\r
- (or\r
-  (not (= (f a (f a a)) a))\r
-  (not (= (f a (f a b)) b))\r
-  (not (= (f a (f a c)) c))\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (not (= (f b (f b a)) a)) \r
-  (not (= (f b (f b b)) b))\r
-  (not (= (f b (f b c)) c))\r
-  ))\r
-\r
-(assert\r
- (or\r
-  (not (= (f c (f c a)) a)) \r
-  (not (= (f c (f c b)) b))\r
-  (not (= (f c (f c c)) c))\r
-  ))\r
-\r
-\r
-(assert  (not (= (f a a) (f b a))))\r
-(assert  (not (= (f a a) (f c a))))\r
-(assert  (not (= (f b a) (f c a))))\r
-\r
-(assert  (not (= (f a b) (f b b))))\r
-(assert  (not (= (f a b) (f c b))))\r
-(assert  (not (= (f b b) (f c b))))\r
-\r
-(assert  (not (= (f a c) (f b c))))\r
-(assert  (not (= (f a c) (f c c))))\r
-(assert  (not (= (f b c) (f c c))))\r
-\r
-\r
-\r
-(check-sat)\r
-\r
-(exit)\r
+(set-logic QF_UF)
+(set-info :status unsat)
+
+(declare-sort I 0)
+(declare-fun f (I I) I)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+
+
+
+(assert
+ (or
+  (= (f a a) a)
+  (= (f a a) b)
+  (= (f a a) c)
+  ))
+
+(assert
+ (or
+  (= (f a b) a)
+  (= (f a b) b)
+  (= (f a b) c)
+  ))
+
+(assert
+ (or
+  (= (f a c) a)
+  (= (f a c) b)
+  (= (f a c) c)
+  ))
+
+(assert
+ (or
+  (= (f b a) a)
+  (= (f b a) b)
+  (= (f b a) c)
+  ))
+
+(assert
+ (or
+  (= (f b b) a)
+  (= (f b b) b)
+  (= (f b b) c)
+  ))
+
+(assert
+ (or
+  (= (f b c) a)
+  (= (f b c) b)
+  (= (f b c) c)
+  ))
+
+
+(assert
+ (or
+  (= (f c a) a)
+  (= (f c a) b)
+  (= (f c a) c)
+  ))
+
+(assert
+ (or
+  (= (f c b) a)
+  (= (f c b) b)
+  (= (f c b) c)
+  ))
+
+(assert
+ (or
+  (= (f c c) a)
+  (= (f c c) b)
+  (= (f c c) c)
+  ))
+
+
+
+(assert
+ (or
+  (= (f a a) a)
+  (= (f b b) a)
+  (= (f c c) a)
+  ))
+
+(assert
+ (or
+  (= (f a a) b)
+  (= (f b b) b)
+  (= (f c c) b)
+  ))
+
+(assert
+ (or
+  (= (f a a) c)
+  (= (f b b) c)
+  (= (f c c) c)
+  ))
+
+
+
+(assert
+ (or
+  (= (f a a) a)
+  (= (f b a) b)
+  (= (f c a) c)
+  ))
+
+(assert
+ (or
+  (= (f a b) a)
+  (= (f b b) b)
+  (= (f c b) c)
+  ))
+
+(assert
+ (or
+  (= (f a c) a)
+  (= (f b c) b)
+  (= (f c c) c)
+  ))
+
+
+
+
+(assert (not (= (f a a) a)))
+(assert (not (= (f b b) b)))
+(assert (not (= (f c c) c)))                
+
+
+(assert
+ (or
+  (not (= (f a (f a a)) a))
+  (not (= (f a (f a b)) b))
+  (not (= (f a (f a c)) c))
+  ))
+
+(assert
+ (or
+  (not (= (f b (f b a)) a)) 
+  (not (= (f b (f b b)) b))
+  (not (= (f b (f b c)) c))
+  ))
+
+(assert
+ (or
+  (not (= (f c (f c a)) a)) 
+  (not (= (f c (f c b)) b))
+  (not (= (f c (f c c)) c))
+  ))
+
+
+(assert  (not (= (f a a) (f b a))))
+(assert  (not (= (f a a) (f c a))))
+(assert  (not (= (f b a) (f c a))))
+
+(assert  (not (= (f a b) (f b b))))
+(assert  (not (= (f a b) (f c b))))
+(assert  (not (= (f b b) (f c b))))
+
+(assert  (not (= (f a c) (f b c))))
+(assert  (not (= (f a c) (f c c))))
+(assert  (not (= (f b c) (f c c))))
+
+
+
+(check-sat)
+
+(exit)