More fixes to model generation, with previously failing testcases

Also refactored some header file includes to reduce compile time

14 files changed, 573 insertions, 80 deletions

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index ec29a407c..d291e79d6 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -21,7 +21,6 @@
 
 #include "theory/theory.h"
 #include "context/context.h"
-#include "theory/model.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index f8e6882a9..17ea7034b 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -18,6 +18,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/model.h"
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::context;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e82a2c75c..a37ed59c8 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -22,6 +22,7 @@
 #include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/model.h"
+
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 72352f6d3..63772cc1f 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -415,6 +415,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   std::set< TypeNode > allTypes;
   eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine);
   for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
+
     // eqc is the equivalence class representative
     Node eqc = (*eqcs_i);
     Trace("model-builder") << "Processing EC: " << eqc << endl;
@@ -470,7 +471,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 
   TypeSet::iterator it;
   set<TypeNode>::iterator type_it;
+  set<Node>::iterator i, i2;
   bool changed, unassignedAssignable, assignOne = false;
+  set<TypeNode> evaluableSet;
 
   // Double-fixed-point loop
   // Outer loop handles a special corner case (see code at end of loop for details)
@@ -482,60 +485,26 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     do {
       changed = false;
       unassignedAssignable = false;
+      evaluableSet.clear();
 
       // Iterate over all types we've seen
       for (type_it = allTypes.begin(); type_it != allTypes.end(); ++type_it) {
         TypeNode t = *type_it;
         TypeNode tb = t.getBaseType();
-        set<Node>::iterator i, i2;
-
-        // 1. First normalize any non-const representative terms for this type
-        set<Node>* repSet = typeRepSet.getSet(tb);
-        bool done = repSet == NULL || repSet->empty();
-        if (!done) {
-          Trace("model-builder") << "  Normalizing base type: " << tb << endl;
-        }
-        while (!done) {
-          done = true;
-          d_normalizedCache.clear();
-          for (i = repSet->begin(); i != repSet->end(); ) {
-            Assert(assertedReps.find(*i) != assertedReps.end());
-            Node rep = assertedReps[*i];
-            Node normalized = normalize(tm, rep, constantReps, false);
-            Trace("model-builder") << "    Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
-            if (normalized.isConst()) {
-              changed = true;
-              done = false;
-              typeConstSet.add(tb, normalized);
-              constantReps[*i] = normalized;
-              assertedReps.erase(*i);
-              i2 = i;
-              ++i;
-              repSet->erase(i2);
-            }
-            else {
-              if (normalized != rep) {
-                assertedReps[*i] = normalized;
-                changed = true;
-                done = false;
-              }
-              ++i;
-            }
-          }
-        }
-
-        // 2. Now try to evaluate or assign the EC's in this type
         set<Node>* noRepSet = typeNoRepSet.getSet(t);
+
+        // 1. Try to evaluate the EC's in this type
         if (noRepSet != NULL && !noRepSet->empty()) {
-          Trace("model-builder") << "   Eval/assign working on type: " << t << endl;
-          bool assignable, evaluable;
+          Trace("model-builder") << "  Eval phase, working on type: " << t << endl;
+          bool assignable, evaluable, evaluated;
           d_normalizedCache.clear();
           for (i = noRepSet->begin(); i != noRepSet->end(); ) {
             i2 = i;
             ++i;
-            eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
             assignable = false;
             evaluable = false;
+            evaluated = false;
+            eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
             for ( ; !eqc_i.isFinished(); ++eqc_i) {
               Node n = *eqc_i;
               if (isAssignable(n)) {
@@ -545,55 +514,138 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
                 evaluable = true;
                 Node normalized = normalize(tm, n, constantReps, true);
                 if (normalized.isConst()) {
-                  typeConstSet.add(t.getBaseType(), normalized);
+                  typeConstSet.add(tb, normalized);
                   constantReps[*i2] = normalized;
                   Trace("model-builder") << "    Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
                   changed = true;
+                  evaluated = true;
                   noRepSet->erase(i2);
                   break;
                 }
               }
             }
-            if (assignable) {
-              // We are about to make a choice - we have to make sure we have learned everything we can first.  Only make a choice if:
-              // 1. fullModel is true
-              // 2. there are no terms of this type with un-normalized representatives
-              // 3. there are no evaluable terms in this EC
-              // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode, go ahead and make one assignment
-              if (fullModel && (((repSet == NULL || repSet->empty()) && !evaluable) || assignOne)) {
-                assignOne = false;
-                Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
-                Node n;
-                if (t.getCardinality().isInfinite()) {
-                  n = typeConstSet.nextTypeEnum(t, true);
-                }
-                else {
-                  TypeEnumerator te(t);
-                  n = *te;
-                }
-                Assert(!n.isNull());
-                constantReps[*i2] = n;
-                Trace("model-builder") << "    Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
-                changed = true;
-                noRepSet->erase(i2);
+            if (!evaluated) {
+              if (evaluable) {
+                evaluableSet.insert(tb);
               }
-              else {
+              if (assignable) {
                 unassignedAssignable = true;
               }
             }
           }
         }
+
+        // 2. Normalize any non-const representative terms for this type
+        set<Node>* repSet = typeRepSet.getSet(t);
+        if (repSet != NULL && !repSet->empty()) {
+          Trace("model-builder") << "  Normalization phase, working on type: " << t << endl;
+          d_normalizedCache.clear();
+          for (i = repSet->begin(); i != repSet->end(); ) {
+            Assert(assertedReps.find(*i) != assertedReps.end());
+            Node rep = assertedReps[*i];
+            Node normalized = normalize(tm, rep, constantReps, false);
+            Trace("model-builder") << "    Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
+            if (normalized.isConst()) {
+              changed = true;
+              typeConstSet.add(t.getBaseType(), normalized);
+              constantReps[*i] = normalized;
+              assertedReps.erase(*i);
+              i2 = i;
+              ++i;
+              repSet->erase(i2);
+            }
+            else {
+              if (normalized != rep) {
+                assertedReps[*i] = normalized;
+                changed = true;
+              }
+              ++i;
+            }
+          }
+        }
       }
     } while (changed);
-    if (!unassignedAssignable || !fullModel) {
+
+    if (!fullModel || !unassignedAssignable) {
       break;
     }
+
+    // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite
+    // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be
+    // different are different.
+
+    // Only make assignments on a type if:
+    // 1. fullModel is true
+    // 2. there are no terms that share the same base type with un-normalized representatives
+    // 3. there are no terms that share teh same base type that are unevaluated evaluable terms
+    // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
+    changed = false;
+    for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
+      set<Node>& noRepSet = TypeSet::getSet(it);
+      if (noRepSet.empty()) {
+        continue;
+      }
+      TypeNode t = TypeSet::getType(it);
+      TypeNode tb = t.getBaseType();
+      if (!assignOne) {
+        set<Node>* repSet = typeRepSet.getSet(tb);
+        if (repSet != NULL && !repSet->empty()) {
+          continue;
+        }
+        if (evaluableSet.find(tb) != evaluableSet.end()) {
+          continue;
+        }
+      }
+      Trace("model-builder") << "  Assign phase, working on type: " << t << endl;
+      bool assignable, evaluable;
+      for (i = noRepSet.begin(); i != noRepSet.end(); ) {
+        i2 = i;
+        ++i;
+        eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
+        assignable = false;
+        evaluable = false;
+        for ( ; !eqc_i.isFinished(); ++eqc_i) {
+          Node n = *eqc_i;
+          if (isAssignable(n)) {
+            assignable = true;
+          }
+          else {
+            evaluable = true;
+          }
+        }
+        if (assignable) {
+          Assert(!evaluable || assignOne);
+          Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
+          Node n;
+          if (t.getCardinality().isInfinite()) {
+            n = typeConstSet.nextTypeEnum(t, true);
+          }
+          else {
+            TypeEnumerator te(t);
+            n = *te;
+          }
+          Assert(!n.isNull());
+          constantReps[*i2] = n;
+          Trace("model-builder") << "    Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
+          changed = true;
+          noRepSet.erase(i2);
+          if (assignOne) {
+            assignOne = false;
+            break;
+          }
+        }
+      }
+    }
+
     // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency
     // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}.  In this case, neither one will get assigned because we are waiting
     // to be able to evaluate.  But we will never be able to evaluate because the variables that need to be assigned are in
     // these same EC's.  In this case, repeat the whole fixed-point computation with the difference that the first EC
     // that has both assignable and evaluable expressions will get assigned.
-    assignOne = true;
+    if (!changed) {
+      Assert(!assignOne); // check for infinite loop!
+      assignOne = true;
+    }
   }
 
 #ifdef CVC4_ASSERTIONS
diff --git a/src/theory/model.h b/src/theory/model.h
index d17192281..19415ae7b 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -216,6 +216,11 @@ private:
     return n;
   }
 
+  bool empty()
+  {
+    return d_typeSet.empty();
+  }
+
   iterator begin()
   {
     return d_typeSet.begin();
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 4a27b4559..e7a24bb79 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -30,7 +30,6 @@
 #include "theory/rewriterules/rr_inst_match.h"
 #include "util/statistics_registry.h"
 #include "theory/rewriterules/theory_rewriterules_preprocess.h"
-#include "theory/model.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index a8e4485e0..ced845a27 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -261,7 +261,3 @@ Node SharedTermsDatabase::explain(TNode literal) const {
   d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
   return mkAnd(assumptions);
 }
-
-void SharedTermsDatabase::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
-  m->assertEqualityEngine( &d_equalityEngine );
-}
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index a1217d5c6..655918986 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -241,10 +241,6 @@ public:
    */
   theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
 
-  /**
-   * collect model info
-   */
-  void collectModelInfo( theory::TheoryModel* m, bool fullModel );
 protected:
 
   /**
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c65fb7ed7..67830390c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -43,7 +43,6 @@
 #include "util/cvc4_assert.h"
 #include "theory/ite_simplifier.h"
 #include "theory/unconstrained_simplifier.h"
-#include "theory/model.h"
 
 namespace CVC4 {
 
@@ -75,6 +74,8 @@ struct NodeTheoryPairHashFunction {
 
 namespace theory {
   class Instantiator;
+  class TheoryModel;
+  class TheoryEngineModelBuilder;
 }/* CVC4::theory namespace */
 
 class DecisionEngine;
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index edeb6b6ec..0ec89af0b 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -19,6 +19,7 @@
 #include "theory/theory_engine.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/uf/options.h"
+#include "theory/model.h"
 
 //#define ONE_SPLIT_REGION
 //#define DISABLE_QUICK_CLIQUE_CHECKS
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index ed810eaeb..e35f24d13 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -18,7 +18,8 @@ TESTS =	\
 	fuzz01.delta01.smt \
 	fuzz02.smt \
 	fuzz03.smt \
-	fuzz04.smt
+	fuzz04.smt \
+	fuzz05.smt
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/auflia/fuzz05.smt b/test/regress/regress0/auflia/fuzz05.smt
new file mode 100644
index 000000000..538f86ece
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz05.smt
@@ -0,0 +1,183 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:status sat
+:extrafuns ((f0 Int Int Int))
+:extrafuns ((f1 Array Array Array Array))
+:extrapreds ((p0 Int))
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Int))
+:extrafuns ((v2 Int))
+:extrafuns ((v3 Array))
+:formula
+(let (?e4 2)
+(let (?e5 (- v2 v2))
+(let (?e6 (f0 v1 v0))
+(let (?e7 (* ?e6 ?e4))
+(let (?e8 (ite (p0 v2) 1 0))
+(let (?e9 (f1 v3 v3 v3))
+(flet ($e10 (p1 ?e9 v3 v3))
+(flet ($e11 (> ?e7 v1))
+(flet ($e12 (<= ?e8 ?e6))
+(flet ($e13 (p0 ?e8))
+(flet ($e14 (>= v2 v0))
+(flet ($e15 (p0 ?e5))
+(let (?e16 (ite $e12 v3 ?e9))
+(let (?e17 (ite $e15 ?e16 v3))
+(let (?e18 (ite $e11 ?e17 ?e16))
+(let (?e19 (ite $e14 ?e9 ?e9))
+(let (?e20 (ite $e13 ?e16 v3))
+(let (?e21 (ite $e12 v3 ?e19))
+(let (?e22 (ite $e10 ?e16 v3))
+(let (?e23 (ite $e15 ?e5 v0))
+(let (?e24 (ite $e12 v1 ?e6))
+(let (?e25 (ite $e11 ?e6 v0))
+(let (?e26 (ite $e15 ?e25 ?e23))
+(let (?e27 (ite $e12 v1 v0))
+(let (?e28 (ite $e14 ?e23 ?e24))
+(let (?e29 (ite $e10 ?e6 ?e23))
+(let (?e30 (ite $e13 v2 ?e29))
+(let (?e31 (ite $e12 ?e7 ?e25))
+(let (?e32 (ite $e12 ?e8 ?e8))
+(let (?e33 (store v3 ?e27 ?e7))
+(let (?e34 (select ?e21 ?e30))
+(let (?e35 (f1 ?e9 ?e21 ?e18))
+(let (?e36 (f1 ?e9 ?e17 v3))
+(let (?e37 (f1 ?e18 ?e21 ?e19))
+(let (?e38 (f1 ?e33 ?e18 ?e35))
+(let (?e39 (f1 ?e22 ?e22 v3))
+(let (?e40 (f1 ?e18 ?e20 ?e22))
+(let (?e41 (f1 ?e16 ?e33 ?e36))
+(let (?e42 (f0 ?e31 ?e26))
+(let (?e43 (+ ?e25 ?e5))
+(let (?e44 (f0 ?e42 v0))
+(let (?e45 (ite (p0 ?e24) 1 0))
+(let (?e46 (f0 ?e8 v0))
+(let (?e47 (ite (p0 v1) 1 0))
+(let (?e48 (+ ?e23 ?e26))
+(let (?e49 (~ ?e28))
+(let (?e50 (ite (p0 ?e27) 1 0))
+(let (?e51 (~ ?e46))
+(let (?e52 (~ ?e32))
+(let (?e53 (* (~ ?e4) ?e30))
+(let (?e54 (~ ?e29))
+(let (?e55 (- ?e48 ?e31))
+(let (?e56 (* ?e4 ?e7))
+(let (?e57 (f0 ?e29 ?e24))
+(let (?e58 (+ ?e34 v2))
+(let (?e59 (f0 ?e26 ?e50))
+(let (?e60 (f0 ?e6 ?e54))
+(flet ($e61 (p1 ?e38 ?e19 ?e9))
+(flet ($e62 (p1 ?e41 ?e18 ?e40))
+(flet ($e63 (p1 ?e21 ?e35 ?e40))
+(flet ($e64 (p1 ?e16 ?e37 ?e19))
+(flet ($e65 (p1 ?e33 ?e38 ?e18))
+(flet ($e66 (p1 ?e39 ?e20 ?e35))
+(flet ($e67 (p1 ?e38 ?e36 ?e40))
+(flet ($e68 (p1 ?e21 ?e35 ?e20))
+(flet ($e69 (p1 ?e9 ?e33 ?e19))
+(flet ($e70 (p1 ?e18 ?e18 ?e35))
+(flet ($e71 (p1 v3 ?e18 ?e41))
+(flet ($e72 (p1 ?e39 ?e35 v3))
+(flet ($e73 (p1 ?e37 ?e22 ?e38))
+(flet ($e74 (p1 ?e16 ?e9 ?e16))
+(flet ($e75 (p1 ?e17 ?e9 ?e37))
+(flet ($e76 (= ?e53 ?e32))
+(flet ($e77 (>= ?e26 ?e55))
+(flet ($e78 (distinct ?e23 ?e7))
+(flet ($e79 (< ?e28 ?e5))
+(flet ($e80 (<= ?e42 ?e30))
+(flet ($e81 (>= ?e58 ?e50))
+(flet ($e82 (= ?e45 ?e46))
+(flet ($e83 (<= ?e59 ?e32))
+(flet ($e84 (p0 ?e56))
+(flet ($e85 (p0 v2))
+(flet ($e86 (p0 ?e31))
+(flet ($e87 (> ?e25 ?e32))
+(flet ($e88 (= ?e44 ?e54))
+(flet ($e89 (< ?e60 ?e23))
+(flet ($e90 (p0 ?e29))
+(flet ($e91 (distinct v2 ?e6))
+(flet ($e92 (<= ?e59 ?e58))
+(flet ($e93 (= ?e43 ?e47))
+(flet ($e94 (distinct ?e54 v2))
+(flet ($e95 (> ?e8 ?e5))
+(flet ($e96 (distinct ?e59 ?e8))
+(flet ($e97 (distinct ?e48 ?e23))
+(flet ($e98 (> ?e24 ?e60))
+(flet ($e99 (>= ?e34 ?e44))
+(flet ($e100 (< ?e49 ?e7))
+(flet ($e101 (distinct ?e51 ?e53))
+(flet ($e102 (<= ?e52 ?e23))
+(flet ($e103 (<= v1 ?e57))
+(flet ($e104 (>= ?e48 ?e52))
+(flet ($e105 (distinct ?e32 ?e29))
+(flet ($e106 (p0 ?e46))
+(flet ($e107 (<= v0 v0))
+(flet ($e108 (= ?e27 ?e43))
+(flet ($e109 (and $e67 $e107))
+(flet ($e110 (or $e75 $e69))
+(flet ($e111 (implies $e15 $e76))
+(flet ($e112 (xor $e98 $e96))
+(flet ($e113 (and $e78 $e62))
+(flet ($e114 (or $e100 $e77))
+(flet ($e115 (xor $e83 $e12))
+(flet ($e116 (and $e13 $e71))
+(flet ($e117 (xor $e116 $e112))
+(flet ($e118 (not $e86))
+(flet ($e119 (or $e81 $e64))
+(flet ($e120 (iff $e72 $e70))
+(flet ($e121 (iff $e108 $e114))
+(flet ($e122 (or $e88 $e74))
+(flet ($e123 (xor $e105 $e118))
+(flet ($e124 (xor $e103 $e104))
+(flet ($e125 (implies $e93 $e119))
+(flet ($e126 (or $e102 $e90))
+(flet ($e127 (iff $e126 $e89))
+(flet ($e128 (if_then_else $e66 $e109 $e106))
+(flet ($e129 (implies $e85 $e101))
+(flet ($e130 (xor $e110 $e128))
+(flet ($e131 (iff $e63 $e11))
+(flet ($e132 (not $e84))
+(flet ($e133 (not $e68))
+(flet ($e134 (or $e124 $e113))
+(flet ($e135 (if_then_else $e82 $e121 $e94))
+(flet ($e136 (iff $e132 $e80))
+(flet ($e137 (or $e95 $e131))
+(flet ($e138 (and $e129 $e122))
+(flet ($e139 (or $e92 $e135))
+(flet ($e140 (xor $e133 $e139))
+(flet ($e141 (if_then_else $e140 $e91 $e130))
+(flet ($e142 (implies $e117 $e117))
+(flet ($e143 (implies $e14 $e79))
+(flet ($e144 (not $e97))
+(flet ($e145 (and $e120 $e143))
+(flet ($e146 (xor $e134 $e87))
+(flet ($e147 (iff $e125 $e111))
+(flet ($e148 (iff $e147 $e146))
+(flet ($e149 (not $e99))
+(flet ($e150 (or $e145 $e148))
+(flet ($e151 (iff $e149 $e141))
+(flet ($e152 (and $e61 $e61))
+(flet ($e153 (if_then_else $e10 $e142 $e152))
+(flet ($e154 (and $e73 $e115))
+(flet ($e155 (or $e138 $e150))
+(flet ($e156 (and $e127 $e136))
+(flet ($e157 (and $e123 $e137))
+(flet ($e158 (if_then_else $e151 $e155 $e155))
+(flet ($e159 (and $e65 $e153))
+(flet ($e160 (not $e144))
+(flet ($e161 (implies $e156 $e156))
+(flet ($e162 (not $e161))
+(flet ($e163 (if_then_else $e162 $e157 $e159))
+(flet ($e164 (implies $e158 $e154))
+(flet ($e165 (or $e160 $e163))
+(flet ($e166 (not $e164))
+(flet ($e167 (iff $e165 $e165))
+(flet ($e168 (and $e166 $e166))
+(flet ($e169 (and $e168 $e168))
+(flet ($e170 (not $e169))
+(flet ($e171 (iff $e167 $e170))
+$e171
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 352161466..60b3109f1 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -37,7 +37,8 @@ SMT_TESTS = \
 	incorrect1.delta01.smt \
 	incorrect1.delta02.smt \
 	error1.smt \
-	neq-deltacomp.smt
+	neq-deltacomp.smt \
+	fuzz01.smt
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
diff --git a/test/regress/regress0/uflra/fuzz01.smt b/test/regress/regress0/uflra/fuzz01.smt
new file mode 100644
index 000000000..2c6286e3a
--- /dev/null
+++ b/test/regress/regress0/uflra/fuzz01.smt
@@ -0,0 +1,257 @@
+(benchmark fuzzsmt
+:logic QF_UFLRA
+:status sat
+:extrafuns ((f0 Real Real))
+:extrafuns ((f1 Real Real Real Real))
+:extrapreds ((p0 Real Real Real))
+:extrafuns ((v0 Real))
+:extrafuns ((v1 Real))
+:extrafuns ((v2 Real))
+:formula
+(let (?e3 5)
+(let (?e4 2)
+(let (?e5 0)
+(let (?e6 (f1 v0 v1 v0))
+(let (?e7 (f0 v0))
+(let (?e8 (ite (p0 v1 ?e7 v0) 1 0))
+(let (?e9 (ite (p0 ?e8 v1 v0) 1 0))
+(let (?e10 (- ?e9 ?e9))
+(let (?e11 (~ v1))
+(let (?e12 (ite (p0 v0 ?e8 v2) 1 0))
+(let (?e13 (/ ?e5 ?e4))
+(let (?e14 (/ ?e4 ?e4))
+(let (?e15 (~ v0))
+(let (?e16 (* ?e6 (~ ?e3)))
+(flet ($e17 (< ?e8 ?e8))
+(flet ($e18 (<= v0 v1))
+(flet ($e19 (distinct ?e16 ?e15))
+(flet ($e20 (distinct ?e13 ?e12))
+(flet ($e21 (> ?e11 ?e11))
+(flet ($e22 (= v0 ?e11))
+(flet ($e23 (p0 ?e16 ?e13 ?e11))
+(flet ($e24 (> ?e16 ?e12))
+(flet ($e25 (= ?e13 ?e12))
+(flet ($e26 (<= ?e12 ?e12))
+(flet ($e27 (p0 ?e12 ?e12 ?e14))
+(flet ($e28 (distinct ?e7 ?e12))
+(flet ($e29 (>= ?e9 ?e13))
+(flet ($e30 (< v2 v0))
+(flet ($e31 (> v2 v1))
+(flet ($e32 (p0 ?e9 v1 ?e6))
+(flet ($e33 (= ?e16 v2))
+(flet ($e34 (p0 ?e7 ?e12 ?e14))
+(flet ($e35 (distinct ?e12 ?e15))
+(flet ($e36 (>= ?e9 ?e15))
+(flet ($e37 (< ?e11 ?e10))
+(let (?e38 (ite $e24 ?e9 ?e14))
+(let (?e39 (ite $e24 ?e12 ?e6))
+(let (?e40 (ite $e30 ?e15 ?e11))
+(let (?e41 (ite $e32 v1 v2))
+(let (?e42 (ite $e36 v1 ?e39))
+(let (?e43 (ite $e33 ?e10 ?e15))
+(let (?e44 (ite $e19 ?e8 ?e16))
+(let (?e45 (ite $e26 v0 ?e12))
+(let (?e46 (ite $e36 ?e7 ?e14))
+(let (?e47 (ite $e20 ?e40 ?e14))
+(let (?e48 (ite $e26 ?e15 ?e9))
+(let (?e49 (ite $e22 ?e13 ?e13))
+(let (?e50 (ite $e31 ?e16 ?e47))
+(let (?e51 (ite $e30 ?e41 ?e11))
+(let (?e52 (ite $e17 ?e6 ?e9))
+(let (?e53 (ite $e18 ?e46 v2))
+(let (?e54 (ite $e19 ?e9 ?e9))
+(let (?e55 (ite $e37 ?e51 v2))
+(let (?e56 (ite $e28 ?e14 ?e46))
+(let (?e57 (ite $e29 ?e12 ?e14))
+(let (?e58 (ite $e17 ?e47 ?e7))
+(let (?e59 (ite $e34 ?e46 v2))
+(let (?e60 (ite $e21 ?e55 ?e51))
+(let (?e61 (ite $e24 ?e14 ?e50))
+(let (?e62 (ite $e17 ?e47 ?e61))
+(let (?e63 (ite $e30 ?e45 ?e12))
+(let (?e64 (ite $e35 ?e45 ?e47))
+(let (?e65 (ite $e25 v1 ?e38))
+(let (?e66 (ite $e23 ?e16 ?e59))
+(let (?e67 (ite $e26 ?e61 ?e38))
+(let (?e68 (ite $e27 ?e57 ?e50))
+(flet ($e69 (> v0 ?e12))
+(flet ($e70 (p0 ?e8 ?e66 ?e43))
+(flet ($e71 (<= ?e64 ?e8))
+(flet ($e72 (> ?e49 ?e43))
+(flet ($e73 (>= v0 ?e46))
+(flet ($e74 (<= v1 ?e49))
+(flet ($e75 (< ?e11 ?e38))
+(flet ($e76 (>= v2 ?e10))
+(flet ($e77 (= ?e51 ?e40))
+(flet ($e78 (>= ?e14 ?e50))
+(flet ($e79 (> ?e49 ?e8))
+(flet ($e80 (= ?e47 ?e12))
+(flet ($e81 (> ?e64 ?e54))
+(flet ($e82 (<= ?e48 ?e57))
+(flet ($e83 (> ?e57 ?e54))
+(flet ($e84 (p0 ?e44 ?e39 ?e65))
+(flet ($e85 (< ?e51 ?e11))
+(flet ($e86 (distinct ?e51 ?e53))
+(flet ($e87 (= ?e57 ?e46))
+(flet ($e88 (p0 ?e6 ?e47 ?e41))
+(flet ($e89 (<= ?e58 ?e14))
+(flet ($e90 (>= ?e67 v1))
+(flet ($e91 (<= ?e39 ?e59))
+(flet ($e92 (>= ?e10 v1))
+(flet ($e93 (> ?e10 ?e10))
+(flet ($e94 (<= ?e57 ?e10))
+(flet ($e95 (< ?e47 ?e42))
+(flet ($e96 (>= ?e41 ?e63))
+(flet ($e97 (<= ?e9 ?e14))
+(flet ($e98 (distinct v0 ?e64))
+(flet ($e99 (distinct ?e49 ?e61))
+(flet ($e100 (p0 ?e61 ?e52 v1))
+(flet ($e101 (>= ?e12 ?e6))
+(flet ($e102 (p0 ?e59 ?e57 ?e62))
+(flet ($e103 (distinct ?e66 ?e15))
+(flet ($e104 (<= ?e46 ?e50))
+(flet ($e105 (>= ?e57 ?e46))
+(flet ($e106 (= ?e44 ?e58))
+(flet ($e107 (p0 ?e6 ?e8 ?e40))
+(flet ($e108 (distinct ?e12 ?e58))
+(flet ($e109 (>= ?e56 ?e15))
+(flet ($e110 (< ?e62 ?e44))
+(flet ($e111 (distinct v2 ?e14))
+(flet ($e112 (< ?e44 ?e39))
+(flet ($e113 (= ?e40 ?e11))
+(flet ($e114 (= ?e55 ?e56))
+(flet ($e115 (p0 ?e66 ?e40 ?e62))
+(flet ($e116 (= ?e13 ?e14))
+(flet ($e117 (> ?e59 ?e68))
+(flet ($e118 (p0 ?e45 ?e50 ?e6))
+(flet ($e119 (p0 ?e67 v2 v1))
+(flet ($e120 (= v2 ?e15))
+(flet ($e121 (< ?e42 ?e12))
+(flet ($e122 (distinct ?e52 ?e40))
+(flet ($e123 (= v1 ?e14))
+(flet ($e124 (< ?e13 ?e66))
+(flet ($e125 (= ?e12 ?e61))
+(flet ($e126 (>= ?e66 v0))
+(flet ($e127 (> ?e58 ?e13))
+(flet ($e128 (distinct ?e41 ?e41))
+(flet ($e129 (>= ?e47 ?e16))
+(flet ($e130 (p0 v2 ?e59 ?e62))
+(flet ($e131 (<= ?e12 ?e41))
+(flet ($e132 (> ?e68 ?e51))
+(flet ($e133 (>= ?e59 ?e38))
+(flet ($e134 (< ?e65 ?e13))
+(flet ($e135 (< ?e39 ?e45))
+(flet ($e136 (>= ?e54 ?e16))
+(flet ($e137 (>= ?e62 ?e54))
+(flet ($e138 (p0 ?e59 ?e54 ?e41))
+(flet ($e139 (p0 ?e53 ?e12 ?e45))
+(flet ($e140 (distinct ?e52 ?e14))
+(flet ($e141 (= ?e51 ?e63))
+(flet ($e142 (p0 ?e65 ?e59 ?e64))
+(flet ($e143 (<= ?e52 ?e45))
+(flet ($e144 (p0 ?e49 ?e12 ?e63))
+(flet ($e145 (> ?e39 ?e7))
+(flet ($e146 (>= ?e60 ?e8))
+(flet ($e147 (if_then_else $e78 $e34 $e87))
+(flet ($e148 (iff $e28 $e83))
+(flet ($e149 (or $e19 $e107))
+(flet ($e150 (not $e29))
+(flet ($e151 (or $e25 $e113))
+(flet ($e152 (implies $e82 $e133))
+(flet ($e153 (or $e120 $e30))
+(flet ($e154 (not $e81))
+(flet ($e155 (xor $e26 $e99))
+(flet ($e156 (not $e105))
+(flet ($e157 (xor $e122 $e126))
+(flet ($e158 (implies $e70 $e97))
+(flet ($e159 (iff $e21 $e150))
+(flet ($e160 (iff $e37 $e33))
+(flet ($e161 (if_then_else $e149 $e139 $e129))
+(flet ($e162 (iff $e96 $e18))
+(flet ($e163 (if_then_else $e116 $e36 $e160))
+(flet ($e164 (implies $e125 $e17))
+(flet ($e165 (iff $e74 $e98))
+(flet ($e166 (and $e159 $e110))
+(flet ($e167 (implies $e152 $e31))
+(flet ($e168 (if_then_else $e141 $e86 $e124))
+(flet ($e169 (and $e80 $e118))
+(flet ($e170 (implies $e22 $e154))
+(flet ($e171 (xor $e84 $e153))
+(flet ($e172 (and $e102 $e77))
+(flet ($e173 (and $e164 $e100))
+(flet ($e174 (if_then_else $e134 $e76 $e90))
+(flet ($e175 (and $e157 $e138))
+(flet ($e176 (or $e92 $e158))
+(flet ($e177 (xor $e103 $e130))
+(flet ($e178 (or $e73 $e101))
+(flet ($e179 (if_then_else $e104 $e174 $e27))
+(flet ($e180 (and $e156 $e172))
+(flet ($e181 (implies $e93 $e176))
+(flet ($e182 (xor $e121 $e32))
+(flet ($e183 (and $e148 $e112))
+(flet ($e184 (and $e165 $e165))
+(flet ($e185 (iff $e72 $e162))
+(flet ($e186 (if_then_else $e151 $e23 $e171))
+(flet ($e187 (or $e111 $e94))
+(flet ($e188 (xor $e144 $e177))
+(flet ($e189 (implies $e185 $e188))
+(flet ($e190 (not $e167))
+(flet ($e191 (xor $e115 $e155))
+(flet ($e192 (and $e95 $e179))
+(flet ($e193 (iff $e180 $e182))
+(flet ($e194 (or $e88 $e131))
+(flet ($e195 (iff $e123 $e168))
+(flet ($e196 (xor $e106 $e194))
+(flet ($e197 (iff $e170 $e191))
+(flet ($e198 (iff $e196 $e117))
+(flet ($e199 (and $e71 $e197))
+(flet ($e200 (or $e119 $e108))
+(flet ($e201 (not $e163))
+(flet ($e202 (iff $e183 $e201))
+(flet ($e203 (implies $e178 $e91))
+(flet ($e204 (or $e142 $e175))
+(flet ($e205 (not $e145))
+(flet ($e206 (and $e146 $e132))
+(flet ($e207 (if_then_else $e173 $e147 $e20))
+(flet ($e208 (or $e195 $e166))
+(flet ($e209 (and $e35 $e79))
+(flet ($e210 (if_then_else $e69 $e75 $e184))
+(flet ($e211 (not $e199))
+(flet ($e212 (iff $e204 $e143))
+(flet ($e213 (xor $e161 $e89))
+(flet ($e214 (iff $e114 $e114))
+(flet ($e215 (not $e214))
+(flet ($e216 (xor $e186 $e189))
+(flet ($e217 (implies $e212 $e24))
+(flet ($e218 (xor $e136 $e202))
+(flet ($e219 (not $e213))
+(flet ($e220 (iff $e135 $e198))
+(flet ($e221 (iff $e169 $e128))
+(flet ($e222 (implies $e207 $e187))
+(flet ($e223 (or $e219 $e211))
+(flet ($e224 (and $e223 $e137))
+(flet ($e225 (and $e205 $e109))
+(flet ($e226 (xor $e200 $e220))
+(flet ($e227 (implies $e208 $e226))
+(flet ($e228 (if_then_else $e193 $e222 $e192))
+(flet ($e229 (xor $e227 $e210))
+(flet ($e230 (and $e216 $e217))
+(flet ($e231 (not $e218))
+(flet ($e232 (implies $e225 $e203))
+(flet ($e233 (xor $e221 $e140))
+(flet ($e234 (xor $e224 $e232))
+(flet ($e235 (if_then_else $e233 $e231 $e181))
+(flet ($e236 (if_then_else $e206 $e228 $e215))
+(flet ($e237 (implies $e236 $e85))
+(flet ($e238 (implies $e229 $e235))
+(flet ($e239 (or $e190 $e237))
+(flet ($e240 (or $e234 $e230))
+(flet ($e241 (iff $e238 $e127))
+(flet ($e242 (not $e240))
+(flet ($e243 (iff $e239 $e241))
+(flet ($e244 (if_then_else $e243 $e242 $e243))
+(flet ($e245 (xor $e244 $e244))
+(flet ($e246 (iff $e209 $e245))
+$e246
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+