Fix for fuzzer-found model bug

(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 826e729fc546df5748a38454ffa7d0b53a3b08dc..3880aaad9f37b6f67ea46ab974eb896b94fcc25e 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -210,7 +210,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
 }
 
 /** add term */
-void TheoryModel::addTerm( Node n ){
+void TheoryModel::addTerm(TNode n ){
   Assert(d_equalityEngine.hasTerm(n));
   //must collect UF terms
   if (n.getKind()==APPLY_UF) {
@@ -223,7 +223,7 @@ void TheoryModel::addTerm( Node n ){
 }
 
 /** assert equality */
-void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
+void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){
   if (a == b && polarity) {
     return;
   }
@@ -233,7 +233,7 @@ void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
 }
 
 /** assert predicate */
-void TheoryModel::assertPredicate( Node a, bool polarity ){
+void TheoryModel::assertPredicate(TNode a, bool polarity ){
   if ((a == d_true && polarity) ||
       (a == d_false && (!polarity))) {
     return;
@@ -263,6 +263,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
       predFalse = ee->areEqual(eqc, d_false);
     }
     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+    bool first = true;
+    Node rep;
     for (; !eqc_i.isFinished(); ++eqc_i) {
       if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
         continue;
@@ -274,28 +276,43 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
         else if (predFalse) {
           assertPredicate(*eqc_i, false);
         }
-        else if (eqc != (*eqc_i)) {
-          Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << eqc << "));" << endl;
-          d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null());
-          Assert(d_equalityEngine.consistent());
+        else {
+          if (first) {
+            rep = (*eqc_i);
+            first = false;
+          }
+          else {
+            Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
+            d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null());
+            Assert(d_equalityEngine.consistent());
+          }
         }
       } else {
-        assertEquality(*eqc_i, eqc, true);
+        if (first) {
+          rep = (*eqc_i);
+          first = false;
+        }
+        else {
+          assertEquality(*eqc_i, rep, true);
+        }
       }
     }
   }
 }
 
-void TheoryModel::assertRepresentative( Node n ){
+void TheoryModel::assertRepresentative(TNode n )
+{
   Trace("model-builder-reps") << "Assert rep : " << n << std::endl;
   d_reps[ n ] = n;
 }
 
-bool TheoryModel::hasTerm( Node a ){
+bool TheoryModel::hasTerm(TNode a)
+{
   return d_equalityEngine.hasTerm( a );
 }
 
-Node TheoryModel::getRepresentative( Node a ){
+Node TheoryModel::getRepresentative(TNode a)
+{
   if( d_equalityEngine.hasTerm( a ) ){
     Node r = d_equalityEngine.getRepresentative( a );
     if( d_reps.find( r )!=d_reps.end() ){
@@ -308,7 +325,8 @@ Node TheoryModel::getRepresentative( Node a ){
   }
 }
 
-bool TheoryModel::areEqual( Node a, Node b ){
+bool TheoryModel::areEqual(TNode a, TNode b)
+{
   if( a==b ){
     return true;
   }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
@@ -318,7 +336,8 @@ bool TheoryModel::areEqual( Node a, Node b ){
   }
 }
 
-bool TheoryModel::areDisequal( Node a, Node b ){
+bool TheoryModel::areDisequal(TNode a, TNode b)
+{
   if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
     return d_equalityEngine.areDisequal( a, b, false );
   }else{

diff --git a/src/theory/model.h b/src/theory/model.h
index 7ccbe2fc3ba34f38a90eef8572318d8115546798..e283ee183c24ae8584318e67e255d803b2a8ef0f 100644 (file)
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -90,11 +90,11 @@ public:
     *   such as contraining the interpretation of uninterpretted functions,
     *   and adding n to the equality engine of this model
     */
-  virtual void addTerm( Node n );
+  virtual void addTerm(TNode n);
   /** assert equality holds in the model */
-  void assertEquality( Node a, Node b, bool polarity );
+  void assertEquality(TNode a, TNode b, bool polarity);
   /** assert predicate holds in the model */
-  void assertPredicate( Node a, bool polarity );
+  void assertPredicate(TNode a, bool polarity);
   /** assert all equalities/predicates in equality engine hold in the model */
   void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
   /** assert representative
@@ -103,13 +103,13 @@ public:
     *  case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
     *  functions where fullModel = true.
     */
-  void assertRepresentative( Node n );
+  void assertRepresentative(TNode n);
 public:
   /** general queries */
-  bool hasTerm( Node a );
-  Node getRepresentative( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
+  bool hasTerm(TNode a);
+  Node getRepresentative(TNode a);
+  bool areEqual(TNode a, TNode b);
+  bool areDisequal(TNode a, TNode b);
 public:
   /** get value function for Exprs. */
   Expr getValue( Expr expr ) const;

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index cc4a1556ff797f609bc99fdf81f87e963f07a351..8ed9096c49e5080cab7ac52920e963f2acbee726 100644 (file)
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -20,6 +20,7 @@ TESTS =       \
        fuzz03.smt \
        fuzz04.smt \
        fuzz05.smt \
+       fuzz06.smt \
        a17.smt \
        error72.delta2.smt \
        x2.smt

diff --git a/test/regress/regress0/auflia/fuzz06.smt b/test/regress/regress0/auflia/fuzz06.smt
new file mode 100644 (file)
index 0000000..88c2a9d
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz06.smt
@@ -0,0 +1,349 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:status sat
+:extrafuns ((f0 Int Int))
+:extrafuns ((f1 Array Array Array))
+:extrapreds ((p0 Int))
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Array))
+:formula
+(let (?e2 0)
+(let (?e3 (ite (p0 v0) 1 0))
+(let (?e4 (ite (p0 v0) 1 0))
+(let (?e5 (~ ?e4))
+(let (?e6 (ite (p0 ?e3) 1 0))
+(let (?e7 (f0 ?e3))
+(let (?e8 (* ?e4 (~ ?e2)))
+(let (?e9 (store v1 ?e5 ?e8))
+(let (?e10 (select ?e9 ?e4))
+(let (?e11 (store ?e9 ?e8 ?e7))
+(let (?e12 (select ?e11 ?e10))
+(let (?e13 (f1 ?e11 ?e11))
+(let (?e14 (f1 v1 ?e13))
+(let (?e15 (f1 ?e9 ?e13))
+(flet ($e16 (p1 ?e14 ?e11 ?e15))
+(flet ($e17 (p1 ?e13 ?e15 v1))
+(flet ($e18 (p1 ?e9 ?e9 ?e14))
+(flet ($e19 (p0 ?e7))
+(flet ($e20 (<= v0 ?e4))
+(flet ($e21 (> ?e7 ?e12))
+(flet ($e22 (= ?e7 ?e12))
+(flet ($e23 (distinct ?e6 ?e5))
+(flet ($e24 (p0 ?e7))
+(flet ($e25 (>= ?e3 ?e8))
+(flet ($e26 (< ?e3 ?e7))
+(flet ($e27 (<= ?e7 v0))
+(flet ($e28 (p0 ?e10))
+(let (?e29 (ite $e27 ?e15 ?e13))
+(let (?e30 (ite $e28 ?e14 ?e14))
+(let (?e31 (ite $e26 ?e9 v1))
+(let (?e32 (ite $e17 ?e11 ?e13))
+(let (?e33 (ite $e23 ?e13 ?e13))
+(let (?e34 (ite $e25 ?e14 ?e30))
+(let (?e35 (ite $e22 ?e30 ?e30))
+(let (?e36 (ite $e25 ?e11 ?e31))
+(let (?e37 (ite $e22 ?e14 ?e35))
+(let (?e38 (ite $e19 ?e36 ?e35))
+(let (?e39 (ite $e21 ?e36 ?e9))
+(let (?e40 (ite $e16 ?e39 ?e11))
+(let (?e41 (ite $e28 ?e29 v1))
+(let (?e42 (ite $e25 ?e33 ?e36))
+(let (?e43 (ite $e21 ?e29 ?e9))
+(let (?e44 (ite $e18 ?e30 ?e13))
+(let (?e45 (ite $e18 ?e11 ?e41))
+(let (?e46 (ite $e20 ?e15 ?e34))
+(let (?e47 (ite $e24 ?e40 ?e13))
+(let (?e48 (ite $e26 ?e7 ?e6))
+(let (?e49 (ite $e21 ?e10 ?e6))
+(let (?e50 (ite $e22 v0 ?e8))
+(let (?e51 (ite $e19 ?e5 ?e4))
+(let (?e52 (ite $e16 ?e12 ?e10))
+(let (?e53 (ite $e16 ?e49 ?e8))
+(let (?e54 (ite $e21 ?e3 v0))
+(let (?e55 (ite $e24 ?e51 ?e52))
+(let (?e56 (ite $e23 ?e10 ?e5))
+(let (?e57 (ite $e18 ?e50 ?e49))
+(let (?e58 (ite $e17 ?e10 ?e4))
+(let (?e59 (ite $e27 ?e57 ?e12))
+(let (?e60 (ite $e21 ?e10 ?e3))
+(let (?e61 (ite $e28 ?e7 ?e55))
+(let (?e62 (ite $e20 ?e53 ?e53))
+(let (?e63 (ite $e25 ?e48 ?e8))
+(let (?e64 (store ?e45 ?e49 ?e8))
+(let (?e65 (store ?e43 ?e55 ?e57))
+(let (?e66 (select ?e34 v0))
+(let (?e67 (store ?e9 ?e66 ?e54))
+(let (?e68 (select ?e64 ?e56))
+(let (?e69 (f1 ?e11 ?e30))
+(let (?e70 (f1 ?e34 ?e36))
+(let (?e71 (f1 ?e38 ?e39))
+(let (?e72 (f1 ?e31 ?e45))
+(let (?e73 (f1 ?e43 ?e43))
+(let (?e74 (f1 ?e37 ?e65))
+(let (?e75 (f1 ?e9 ?e38))
+(let (?e76 (f1 ?e37 ?e14))
+(let (?e77 (f1 ?e13 ?e39))
+(let (?e78 (f1 ?e34 ?e39))
+(let (?e79 (f1 ?e64 ?e64))
+(let (?e80 (f1 ?e15 ?e15))
+(let (?e81 (f1 v1 v1))
+(let (?e82 (f1 ?e47 ?e71))
+(let (?e83 (f1 ?e77 ?e13))
+(let (?e84 (f1 ?e32 ?e32))
+(let (?e85 (f1 ?e46 ?e46))
+(let (?e86 (f1 ?e36 ?e72))
+(let (?e87 (f1 ?e81 ?e65))
+(let (?e88 (f1 ?e29 ?e45))
+(let (?e89 (f1 ?e44 ?e31))
+(let (?e90 (f1 ?e41 ?e41))
+(let (?e91 (f1 ?e34 ?e42))
+(let (?e92 (f1 ?e35 ?e35))
+(let (?e93 (f1 ?e33 ?e33))
+(let (?e94 (f1 ?e11 ?e14))
+(let (?e95 (f1 ?e67 ?e34))
+(let (?e96 (f1 ?e86 ?e37))
+(let (?e97 (f1 ?e40 ?e40))
+(let (?e98 (- ?e56 ?e5))
+(let (?e99 (+ ?e52 ?e57))
+(let (?e100 (ite (p0 ?e51) 1 0))
+(let (?e101 (ite (p0 ?e12) 1 0))
+(let (?e102 (ite (p0 ?e58) 1 0))
+(let (?e103 (+ v0 ?e10))
+(let (?e104 (~ ?e48))
+(let (?e105 (* ?e2 ?e12))
+(let (?e106 (- ?e3 ?e101))
+(let (?e107 (- ?e59 ?e100))
+(let (?e108 (ite (p0 ?e10) 1 0))
+(let (?e109 (* ?e2 ?e102))
+(let (?e110 (ite (p0 ?e7) 1 0))
+(let (?e111 (* ?e53 (~ ?e2)))
+(let (?e112 (* ?e2 ?e4))
+(let (?e113 (~ ?e106))
+(let (?e114 (~ ?e57))
+(let (?e115 (* ?e68 (~ ?e2)))
+(let (?e116 (- ?e4 ?e50))
+(let (?e117 (* ?e2 ?e49))
+(let (?e118 (ite (p0 ?e61) 1 0))
+(let (?e119 (ite (p0 ?e62) 1 0))
+(let (?e120 (* ?e10 ?e2))
+(let (?e121 (ite (p0 ?e119) 1 0))
+(let (?e122 (f0 ?e55))
+(let (?e123 (* (~ ?e2) ?e66))
+(let (?e124 (* ?e2 ?e63))
+(let (?e125 (ite (p0 ?e106) 1 0))
+(let (?e126 (f0 ?e102))
+(let (?e127 (f0 ?e55))
+(let (?e128 (f0 ?e103))
+(let (?e129 (~ ?e8))
+(let (?e130 (- ?e126 ?e6))
+(let (?e131 (* (~ ?e2) ?e60))
+(let (?e132 (* (~ ?e2) ?e54))
+(flet ($e133 (p1 ?e15 ?e73 ?e14))
+(flet ($e134 (p1 ?e47 ?e78 ?e81))
+(flet ($e135 (p1 ?e44 ?e80 ?e37))
+(flet ($e136 (p1 ?e42 ?e73 ?e91))
+(flet ($e137 (p1 ?e43 ?e37 ?e14))
+(flet ($e138 (p1 ?e73 ?e87 ?e34))
+(flet ($e139 (p1 ?e75 ?e46 ?e75))
+(flet ($e140 (p1 ?e96 ?e96 ?e88))
+(flet ($e141 (p1 ?e89 ?e78 ?e87))
+(flet ($e142 (p1 ?e70 ?e95 ?e47))
+(flet ($e143 (p1 ?e39 ?e96 ?e74))
+(flet ($e144 (p1 ?e91 ?e72 ?e70))
+(flet ($e145 (p1 v1 ?e65 ?e44))
+(flet ($e146 (p1 ?e90 ?e70 ?e79))
+(flet ($e147 (p1 ?e94 ?e91 ?e13))
+(flet ($e148 (p1 ?e41 ?e93 ?e32))
+(flet ($e149 (p1 ?e40 ?e91 ?e93))
+(flet ($e150 (p1 ?e92 ?e34 ?e80))
+(flet ($e151 (p1 ?e71 ?e44 ?e78))
+(flet ($e152 (p1 ?e43 ?e34 ?e73))
+(flet ($e153 (p1 ?e81 ?e73 ?e70))
+(flet ($e154 (p1 ?e86 ?e86 ?e38))
+(flet ($e155 (p1 ?e45 v1 ?e36))
+(flet ($e156 (p1 ?e43 ?e30 ?e37))
+(flet ($e157 (p1 ?e84 ?e78 ?e45))
+(flet ($e158 (p1 ?e67 ?e38 ?e90))
+(flet ($e159 (p1 ?e31 ?e81 ?e13))
+(flet ($e160 (p1 ?e64 ?e47 ?e94))
+(flet ($e161 (p1 ?e29 ?e75 ?e76))
+(flet ($e162 (p1 ?e85 ?e96 ?e82))
+(flet ($e163 (p1 ?e33 ?e29 ?e38))
+(flet ($e164 (p1 ?e31 ?e78 ?e69))
+(flet ($e165 (p1 ?e97 ?e9 ?e35))
+(flet ($e166 (p1 ?e83 ?e71 ?e79))
+(flet ($e167 (p1 ?e11 ?e67 ?e31))
+(flet ($e168 (p1 ?e39 ?e93 ?e96))
+(flet ($e169 (p1 ?e65 ?e85 ?e44))
+(flet ($e170 (p1 ?e76 ?e40 ?e15))
+(flet ($e171 (p1 ?e77 ?e34 ?e14))
+(flet ($e172 (distinct ?e129 ?e62))
+(flet ($e173 (p0 ?e116))
+(flet ($e174 (> ?e120 ?e10))
+(flet ($e175 (p0 ?e102))
+(flet ($e176 (> ?e50 ?e53))
+(flet ($e177 (> ?e119 ?e127))
+(flet ($e178 (distinct ?e117 ?e55))
+(flet ($e179 (= ?e122 ?e102))
+(flet ($e180 (< ?e123 ?e52))
+(flet ($e181 (> ?e66 ?e51))
+(flet ($e182 (= ?e121 ?e4))
+(flet ($e183 (distinct ?e130 ?e102))
+(flet ($e184 (< ?e111 ?e4))
+(flet ($e185 (p0 ?e68))
+(flet ($e186 (distinct ?e3 ?e3))
+(flet ($e187 (>= ?e66 ?e59))
+(flet ($e188 (< ?e10 ?e48))
+(flet ($e189 (distinct ?e5 ?e52))
+(flet ($e190 (= ?e101 ?e54))
+(flet ($e191 (>= ?e8 ?e116))
+(flet ($e192 (<= ?e62 ?e12))
+(flet ($e193 (< ?e131 ?e114))
+(flet ($e194 (>= ?e49 ?e125))
+(flet ($e195 (> ?e100 ?e7))
+(flet ($e196 (p0 ?e101))
+(flet ($e197 (distinct ?e118 ?e52))
+(flet ($e198 (<= v0 ?e60))
+(flet ($e199 (p0 ?e128))
+(flet ($e200 (>= ?e6 ?e106))
+(flet ($e201 (= ?e50 ?e61))
+(flet ($e202 (> ?e115 ?e132))
+(flet ($e203 (distinct ?e57 ?e102))
+(flet ($e204 (>= ?e102 ?e55))
+(flet ($e205 (p0 ?e55))
+(flet ($e206 (<= ?e113 ?e132))
+(flet ($e207 (<= ?e124 ?e106))
+(flet ($e208 (> ?e68 ?e117))
+(flet ($e209 (p0 ?e56))
+(flet ($e210 (<= ?e63 ?e112))
+(flet ($e211 (<= ?e119 ?e5))
+(flet ($e212 (= ?e105 ?e51))
+(flet ($e213 (< ?e6 ?e118))
+(flet ($e214 (p0 ?e66))
+(flet ($e215 (>= ?e58 ?e101))
+(flet ($e216 (distinct ?e109 ?e57))
+(flet ($e217 (distinct ?e99 ?e103))
+(flet ($e218 (<= ?e126 ?e58))
+(flet ($e219 (>= ?e107 ?e120))
+(flet ($e220 (< ?e125 ?e124))
+(flet ($e221 (> ?e98 ?e105))
+(flet ($e222 (p0 ?e118))
+(flet ($e223 (= ?e108 ?e4))
+(flet ($e224 (= ?e58 ?e114))
+(flet ($e225 (< ?e110 ?e123))
+(flet ($e226 (distinct ?e104 ?e111))
+(flet ($e227 (iff $e179 $e21))
+(flet ($e228 (if_then_else $e185 $e171 $e141))
+(flet ($e229 (and $e152 $e216))
+(flet ($e230 (and $e133 $e165))
+(flet ($e231 (and $e155 $e217))
+(flet ($e232 (iff $e16 $e180))
+(flet ($e233 (if_then_else $e168 $e191 $e153))
+(flet ($e234 (implies $e159 $e147))
+(flet ($e235 (not $e203))
+(flet ($e236 (xor $e28 $e223))
+(flet ($e237 (and $e174 $e172))
+(flet ($e238 (or $e194 $e197))
+(flet ($e239 (iff $e149 $e201))
+(flet ($e240 (not $e181))
+(flet ($e241 (or $e238 $e157))
+(flet ($e242 (and $e190 $e225))
+(flet ($e243 (implies $e140 $e215))
+(flet ($e244 (xor $e176 $e20))
+(flet ($e245 (not $e241))
+(flet ($e246 (iff $e243 $e158))
+(flet ($e247 (iff $e18 $e169))
+(flet ($e248 (xor $e173 $e210))
+(flet ($e249 (if_then_else $e212 $e143 $e218))
+(flet ($e250 (not $e177))
+(flet ($e251 (or $e207 $e163))
+(flet ($e252 (implies $e214 $e156))
+(flet ($e253 (or $e170 $e166))
+(flet ($e254 (iff $e206 $e209))
+(flet ($e255 (and $e231 $e189))
+(flet ($e256 (or $e148 $e167))
+(flet ($e257 (if_then_else $e237 $e248 $e235))
+(flet ($e258 (or $e138 $e142))
+(flet ($e259 (or $e249 $e164))
+(flet ($e260 (and $e208 $e204))
+(flet ($e261 (xor $e260 $e202))
+(flet ($e262 (xor $e193 $e136))
+(flet ($e263 (if_then_else $e184 $e219 $e227))
+(flet ($e264 (not $e145))
+(flet ($e265 (or $e256 $e187))
+(flet ($e266 (implies $e160 $e205))
+(flet ($e267 (iff $e178 $e134))
+(flet ($e268 (or $e220 $e27))
+(flet ($e269 (and $e265 $e25))
+(flet ($e270 (not $e242))
+(flet ($e271 (or $e270 $e255))
+(flet ($e272 (not $e199))
+(flet ($e273 (xor $e239 $e154))
+(flet ($e274 (or $e144 $e144))
+(flet ($e275 (if_then_else $e267 $e230 $e258))
+(flet ($e276 (not $e22))
+(flet ($e277 (and $e17 $e192))
+(flet ($e278 (and $e246 $e135))
+(flet ($e279 (and $e228 $e234))
+(flet ($e280 (and $e232 $e263))
+(flet ($e281 (and $e268 $e269))
+(flet ($e282 (if_then_else $e188 $e229 $e183))
+(flet ($e283 (if_then_else $e150 $e276 $e236))
+(flet ($e284 (if_then_else $e252 $e24 $e211))
+(flet ($e285 (iff $e264 $e151))
+(flet ($e286 (xor $e200 $e175))
+(flet ($e287 (or $e281 $e250))
+(flet ($e288 (if_then_else $e262 $e262 $e280))
+(flet ($e289 (not $e26))
+(flet ($e290 (if_then_else $e245 $e259 $e245))
+(flet ($e291 (not $e162))
+(flet ($e292 (if_then_else $e266 $e251 $e289))
+(flet ($e293 (implies $e254 $e275))
+(flet ($e294 (or $e273 $e293))
+(flet ($e295 (xor $e272 $e224))
+(flet ($e296 (implies $e257 $e240))
+(flet ($e297 (iff $e253 $e23))
+(flet ($e298 (iff $e19 $e292))
+(flet ($e299 (implies $e282 $e196))
+(flet ($e300 (iff $e284 $e139))
+(flet ($e301 (implies $e297 $e283))
+(flet ($e302 (and $e291 $e221))
+(flet ($e303 (not $e247))
+(flet ($e304 (xor $e294 $e161))
+(flet ($e305 (not $e244))
+(flet ($e306 (iff $e290 $e279))
+(flet ($e307 (and $e300 $e182))
+(flet ($e308 (implies $e288 $e195))
+(flet ($e309 (if_then_else $e304 $e299 $e186))
+(flet ($e310 (if_then_else $e261 $e222 $e213))
+(flet ($e311 (or $e286 $e301))
+(flet ($e312 (and $e311 $e298))
+(flet ($e313 (and $e295 $e302))
+(flet ($e314 (if_then_else $e305 $e278 $e278))
+(flet ($e315 (not $e226))
+(flet ($e316 (not $e303))
+(flet ($e317 (not $e315))
+(flet ($e318 (and $e296 $e137))
+(flet ($e319 (if_then_else $e307 $e308 $e313))
+(flet ($e320 (xor $e233 $e319))
+(flet ($e321 (if_then_else $e317 $e310 $e274))
+(flet ($e322 (not $e146))
+(flet ($e323 (xor $e198 $e321))
+(flet ($e324 (implies $e316 $e271))
+(flet ($e325 (xor $e312 $e314))
+(flet ($e326 (implies $e285 $e306))
+(flet ($e327 (if_then_else $e324 $e325 $e325))
+(flet ($e328 (if_then_else $e322 $e287 $e326))
+(flet ($e329 (implies $e323 $e309))
+(flet ($e330 (if_then_else $e327 $e329 $e318))
+(flet ($e331 (if_then_else $e277 $e330 $e277))
+(flet ($e332 (not $e328))
+(flet ($e333 (implies $e332 $e332))
+(flet ($e334 (not $e320))
+(flet ($e335 (implies $e333 $e334))
+(flet ($e336 (xor $e335 $e335))
+(flet ($e337 (iff $e331 $e336))
+$e337
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+