From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 12 Jul 2011 22:42:15 +0000 (+0000)
Subject: fix bug 272, array unsoundness, and some array cleanup
X-Git-Tag: cvc5-1.0.0~8495
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=95983dc012aa455b856f320ddcd4cfaf7c6a4582;p=cvc5.git

fix bug 272, array unsoundness, and some array cleanup
---

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index c795de0b9..5a836fdc2 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -34,20 +34,20 @@ bool inList(const CTNodeList* l, const TNode el) {
 
 void printList (CTNodeList* list) {
   CTNodeList::const_iterator it = list->begin();
-  Debug("arrays-info")<<"   [ ";
+  Trace("arrays-info")<<"   [ ";
   for(; it != list->end(); it++ ) {
-    Debug("arrays-info")<<(*it)<<" ";
+    Trace("arrays-info")<<(*it)<<" ";
   }
-  Debug("arrays-info")<<"] \n";
+  Trace("arrays-info")<<"] \n";
 }
 
 void printList (List<TNode>* list) {
   List<TNode>::const_iterator it = list->begin();
-  Debug("arrays-info")<<"   [ ";
+  Trace("arrays-info")<<"   [ ";
   for(; it != list->end(); it++ ) {
-    Debug("arrays-info")<<(*it)<<" ";
+    Trace("arrays-info")<<(*it)<<" ";
   }
-  Debug("arrays-info")<<"] \n";
+  Trace("arrays-info")<<"] \n";
 }
 
 void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
@@ -67,7 +67,7 @@ void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
 void ArrayInfo::addIndex(const Node a, const TNode i) {
   Assert(a.getType().isArray());
   Assert(!i.getType().isArray()); // temporary for flat arrays
-  Debug("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
+  Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
   List<TNode>* temp_indices;
   Info* temp_info;
 
@@ -84,7 +84,7 @@ void ArrayInfo::addIndex(const Node a, const TNode i) {
     temp_indices = (*it).second->indices;
     temp_indices->append(i);
   }
-  if(Debug.isOn("arrays-ind")) {
+  if(Trace.isOn("arrays-ind")) {
     printList((*(info_map.find(a))).second->indices);
   }
 
@@ -115,7 +115,7 @@ void ArrayInfo::addStore(const Node a, const TNode st){
 
 
 void ArrayInfo::addInStore(const TNode a, const TNode b){
-  Debug("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
+  Trace("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
   Assert(a.getType().isArray());
   Assert(b.getType().isArray());
 
@@ -182,20 +182,20 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){
   TimerStat::CodeTimer codeTimer(d_mergeInfoTimer);
   ++d_callsMergeInfo;
 
-  Debug("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
-  Debug("arrays-mergei")<<"                      and "<<b<<"\n";
+  Trace("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
+  Trace("arrays-mergei")<<"                      and "<<b<<"\n";
 
   CNodeInfoMap::iterator ita = info_map.find(a);
   CNodeInfoMap::iterator itb = info_map.find(b);
 
   if(ita != info_map.end()) {
-    Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
-    if(Debug.isOn("arrays-mergei"))
+    Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
+    if(Trace.isOn("arrays-mergei"))
       (*ita).second->print();
 
     if(itb != info_map.end()) {
-      Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
-      if(Debug.isOn("arrays-mergei"))
+      Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
+      if(Trace.isOn("arrays-mergei"))
         (*itb).second->print();
 
       List<TNode>* lista_i = (*ita).second->indices;
@@ -241,9 +241,9 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){
     }
 
   } else {
-    Debug("arrays-mergei")<<" First element has no info \n";
+    Trace("arrays-mergei")<<" First element has no info \n";
     if(itb != info_map.end()) {
-      Debug("arrays-mergei")<<" adding second element's info \n";
+      Trace("arrays-mergei")<<" adding second element's info \n";
       (*itb).second->print();
 
       List<TNode>* listb_i = (*itb).second->indices;
@@ -258,11 +258,11 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){
       info_map[a] = temp_info;
 
     } else {
-    Debug("arrays-mergei")<<" Second element has no info \n";
+    Trace("arrays-mergei")<<" Second element has no info \n";
     }
 
    }
-  Debug("arrays-mergei")<<"Arrays::mergeInfo done \n";
+  Trace("arrays-mergei")<<"Arrays::mergeInfo done \n";
 
 }
 
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 6eb20e30a..ce3f015b5 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -85,11 +85,11 @@ public:
    */
   void print() const {
     Assert(indices != NULL && stores!= NULL); // && equals != NULL);
-    Debug("arrays-info")<<"  indices   ";
+    Trace("arrays-info")<<"  indices   ";
     printList(indices);
-    Debug("arrays-info")<<"  stores ";
+    Trace("arrays-info")<<"  stores ";
     printList(stores);
-    Debug("arrays-info")<<"  in_stores ";
+    Trace("arrays-info")<<"  in_stores ";
     printList(in_stores);
   }
 };
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dab78c17a..888a98a45 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -76,7 +76,7 @@ TheoryArrays::~TheoryArrays() {
 
 
 void TheoryArrays::addSharedTerm(TNode t) {
-  Debug("arrays") << "Arrays::addSharedTerm(): "
+  Trace("arrays") << "Arrays::addSharedTerm(): "
                   << t << endl;
 }
 
@@ -85,7 +85,7 @@ void TheoryArrays::notifyEq(TNode lhs, TNode rhs) {
 }
 
 void TheoryArrays::notifyCongruent(TNode a, TNode b) {
-  Debug("arrays") << "Arrays::notifyCongruent(): "
+  Trace("arrays") << "Arrays::notifyCongruent(): "
        << a << " = " << b << endl;
   if(!d_conflict.isNull()) {
     return;
@@ -103,10 +103,10 @@ void TheoryArrays::check(Effort e) {
    return;
   }
 
-  Debug("arrays") <<"Arrays::start check ";
+  Trace("arrays") <<"Arrays::start check ";
   while(!done()) {
     Node assertion = get();
-    Debug("arrays") << "Arrays::check(): " << assertion << endl;
+    Trace("arrays") << "Arrays::check(): " << assertion << endl;
 
     switch(assertion.getKind()) {
     case kind::EQUAL:
@@ -143,6 +143,7 @@ void TheoryArrays::check(Effort e) {
       }
       else if(find(a) == find(b)) {
         Node conflict = constructConflict(assertion[0]);
+        d_conflict = Node::null();
         d_out->conflict(conflict, false);
         return;
         }
@@ -162,10 +163,10 @@ void TheoryArrays::check(Effort e) {
     // generate the lemmas on the worklist
     //while(!d_RowQueue.empty() || ! d_extQueue.empty()) {
     dischargeLemmas();
-    Debug("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n";
+    Trace("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n";
     //}
   }
-  Debug("arrays") << "Arrays::check(): done" << endl;
+  Trace("arrays") << "Arrays::check(): done" << endl;
 }
 
 Node TheoryArrays::getValue(TNode n) {
@@ -390,7 +391,7 @@ Node TheoryArrays::preprocess(TNode atom) {
 void TheoryArrays::merge(TNode a, TNode b) {
   Assert(d_conflict.isNull());
 
-  Debug("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl;
+  Trace("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl;
 
   /*
    * take care of the congruence closure part
@@ -546,7 +547,7 @@ bool TheoryArrays::isNonLinear(TNode a) {
 }
 
 bool TheoryArrays::isAxiom(TNode t1, TNode t2) {
-  Debug("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n";
+  Trace("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n";
   if(t1.getKind() == kind::SELECT) {
     TNode a = t1[0];
     TNode i = t1[1];
@@ -556,7 +557,7 @@ bool TheoryArrays::isAxiom(TNode t1, TNode t2) {
       TNode j = a[1];
       TNode v = a[2];
       if(i == j && v == t2) {
-        Debug("arrays-axiom")<<"Arrays::isAxiom true\n";
+        Trace("arrays-axiom")<<"Arrays::isAxiom true\n";
         return true;
       }
     }
@@ -566,8 +567,8 @@ bool TheoryArrays::isAxiom(TNode t1, TNode t2) {
 
 
 Node TheoryArrays::constructConflict(TNode diseq) {
-  Debug("arrays") << "arrays: begin constructConflict()" << endl;
-  Debug("arrays") << "arrays:   using diseq == " << diseq << endl;
+  Trace("arrays") << "arrays: begin constructConflict()" << endl;
+  Trace("arrays") << "arrays:   using diseq == " << diseq << endl;
 
   // returns the reason the two terms are equal
   Node explanation = d_cc.explain(diseq[0], diseq[1]);
@@ -594,7 +595,7 @@ Node TheoryArrays::constructConflict(TNode diseq) {
 
   nb<<diseq.notNode();
   Node conflict = nb;
-  Debug("arrays") << "conflict constructed : " << conflict << endl;
+  Trace("arrays") << "conflict constructed : " << conflict << endl;
   return conflict;
 }
 
@@ -665,7 +666,7 @@ void TheoryArrays::addDiseq(TNode diseq) {
 }
 
 void TheoryArrays::appendToDiseqList(TNode of, TNode eq) {
-  Debug("arrays") << "appending " << eq << endl
+  Trace("arrays") << "appending " << eq << endl
               << "  to diseq list of " << of << endl;
   Assert(eq.getKind() == kind::EQUAL ||
          eq.getKind() == kind::IFF);
@@ -688,7 +689,6 @@ void TheoryArrays::appendToDiseqList(TNode of, TNode eq) {
  * Iterates through the indices of a and stores of b and checks if any new
  * Row lemmas need to be instantiated.
  */
-
 bool TheoryArrays::isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j) {
   Assert(a.getType().isArray());
   Assert(b.getType().isArray());
@@ -707,61 +707,78 @@ bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) {
   Node bj = nm->mkNode(kind::SELECT, b, j);
 
   if(find(i) == find(j) || find(aj) == find(bj)) {
-    //Debug("arrays-lem")<<"isRedundantInContext valid "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
-    checkRowForIndex(j,b); // why am i doing this?
-    checkRowForIndex(i,a);
+    Trace("arrays") << "isRedundantInContext valid "
+                    << a << " " << b << " " << i << " " << j << endl;
+    checkRowForIndex(j, b); // why am i doing this?
+    checkRowForIndex(i, a);
     return true;
   }
-  Node literal1 = Rewriter::rewrite(i.eqNode(j));
+  Trace("arrays") << "isRedundantInContext " << a << endl
+                  << "isRedundantInContext " << b << endl
+                  << "isRedundantInContext " << i << endl
+                  << "isRedundantInContext " << j << endl;
+  Node ieqj = i.eqNode(j);
+  Node literal1 = Rewriter::rewrite(ieqj);
   bool hasValue1, satValue1;
   Node ff = nm->mkConst<bool>(false);
   Node tt = nm->mkConst<bool>(true);
   if (literal1 == ff) {
     hasValue1 = true;
     satValue1 = false;
-  }
-  else if (literal1 == tt) {
+  } else if (literal1 == tt) {
     hasValue1 = true;
     satValue1 = true;
+  } else {
+    hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1));
   }
-  else hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1));
   if (hasValue1) {
-    if (satValue1) return true;
-    Node literal2 = Rewriter::rewrite(aj.eqNode(bj));
+    if (satValue1) {
+      Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl;
+      return true;
+    }
+    Node ajeqbj = aj.eqNode(bj);
+    Node literal2 = Rewriter::rewrite(ajeqbj);
     bool hasValue2, satValue2;
     if (literal2 == ff) {
       hasValue2 = true;
       satValue2 = false;
-    }
-    else if (literal2 == tt) {
+    } else if (literal2 == tt) {
       hasValue2 = true;
       satValue2 = true;
+    } else {
+      hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2));
     }
-    else hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2));
     if (hasValue2) {
-      if (satValue2) return true;
+      if (satValue2) {
+        Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl;
+        return true;
+      }
       // conflict
       Assert(!satValue1 && !satValue2);
       Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL);
       NodeBuilder<2> nb(kind::AND);
-      literal1 = areDisequal(literal1[0],literal1[1]);
-      literal2 = areDisequal(literal2[0],literal2[1]);
+      //literal1 = areDisequal(literal1[0], literal1[1]);
+      //literal2 = areDisequal(literal2[0], literal2[1]);
       Assert(!literal1.isNull() && !literal2.isNull());
       nb << literal1.notNode() << literal2.notNode();
       literal1 = nb;
+      d_conflict = Node::null();
       d_out->conflict(literal1, false);
+      Trace("arrays") << "TheoryArrays::isRedundantInContext() "
+                      << "conflict via lemma: " << literal1 << endl;
       return true;
     }
   }
-  if(alreadyAddedRow(a,b,i,j)) {
-   // Debug("arrays-lem")<<"isRedundantInContext already added "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+  if(alreadyAddedRow(a, b, i, j)) {
+    Trace("arrays") << "isRedundantInContext already added "
+                    << a << " " << b << " " << i << " " << j << endl;
     return true;
   }
   return false;
 }
 
 TNode TheoryArrays::areDisequal(TNode a, TNode b) {
-  Debug("arrays-prop")<<"Arrays::areDisequal "<<a<<" "<<b<<"\n";
+  Trace("arrays-prop") << "Arrays::areDisequal " << a << " " << b << "\n";
 
   a = find(a);
   b = find(b);
@@ -770,7 +787,7 @@ TNode TheoryArrays::areDisequal(TNode a, TNode b) {
   if(it!= d_disequalities.end()) {
     CTNodeListAlloc::const_iterator i = (*it).second->begin();
     for( ; i!= (*it).second->end(); i++) {
-      Debug("arrays-prop")<<"   "<<*i<<"\n";
+      Trace("arrays-prop") << "   " << *i << "\n";
       TNode s = (*i)[0];
       TNode t = (*i)[1];
 
@@ -791,12 +808,12 @@ TNode TheoryArrays::areDisequal(TNode a, TNode b) {
 
     }
   }
-  Debug("arrays-prop")<<"    not disequal \n";
+  Trace("arrays-prop") << "    not disequal \n";
   return TNode::null();
 }
 
 bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
-  Debug("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+  Trace("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
 
   NodeManager* nm = NodeManager::currentNM();
   Node aj = nm->mkNode(kind::SELECT, a, j);
@@ -816,7 +833,7 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
     // check if the current context implies that (NOT i = j)
     if(diseq != TNode::null()) {
       // if it's unassigned
-      Debug("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull();
+      Trace("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull();
       if(d_valuation.getSatValue(eq_aj_bj).isNull()) {
         d_out->propagate(eq_aj_bj);
         ++d_numProp;
@@ -848,14 +865,14 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
     }
   }
 
-  Debug("arrays-prop")<<"Arrays::propagateFromRow no prop \n";
+  Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n";
   return false;
 }
 
 void TheoryArrays::explain(TNode n) {
 
 
-  Debug("arrays")<<"Arrays::explain start for "<<n<<"\n";
+  Trace("arrays")<<"Arrays::explain start for "<<n<<"\n";
   ++d_numExplain;
 
   Assert(n.getKind()==kind::EQUAL);
@@ -938,17 +955,17 @@ void TheoryArrays::explain(TNode n) {
   nb << diseq;
   Node reason = nb;
   d_out->explanation(reason);
-  Debug("arrays")<<"explanation "<< reason<<" done \n";
+  Trace("arrays")<<"explanation "<< reason<<" done \n";
   */
 }
 
 void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
 
-  Debug("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
-  if(Debug.isOn("arrays-crl"))
+  Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
+  if(Trace.isOn("arrays-crl"))
     d_infoMap.getInfo(a)->print();
-  Debug("arrays-crl")<<"  ------------  and "<<b<<"\n";
-  if(Debug.isOn("arrays-crl"))
+  Trace("arrays-crl")<<"  ------------  and "<<b<<"\n";
+  if(Trace.isOn("arrays-crl"))
     d_infoMap.getInfo(b)->print();
 
   List<TNode>* i_a = d_infoMap.getIndices(a);
@@ -995,7 +1012,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
     }
   }
 
-  Debug("arrays-crl")<<"Arrays::checkLemmas done.\n";
+  Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
 /**
@@ -1018,7 +1035,7 @@ inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) {
 
 
 
- Debug("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
+ Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
  d_RowAlreadyAdded.insert(make_quad(a,b,i,j));
  d_out->lemma(lem);
  ++d_numRow;
@@ -1032,10 +1049,10 @@ inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) {
  * store(a _ _ )
  */
 void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
-  Debug("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
-  Debug("arrays-cri")<<"                   index "<<i<<"\n";
+  Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
+  Trace("arrays-cri")<<"                   index "<<i<<"\n";
 
-  if(Debug.isOn("arrays-cri")) {
+  if(Trace.isOn("arrays-cri")) {
     d_infoMap.getInfo(a)->print();
   }
   Assert(a.getType().isArray());
@@ -1048,9 +1065,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
     TNode store = *it;
     Assert(store.getKind()==kind::STORE);
     TNode j = store[1];
-    //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+    //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
     if(!isRedundandRowLemma(store, store[0], j, i)) {
-      //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+      //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(store, store[0], j, i);
     }
   }
@@ -1060,9 +1077,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
     TNode instore = *it;
     Assert(instore.getKind()==kind::STORE);
     TNode j = instore[1];
-    //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+    //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
     if(!isRedundandRowLemma(instore, instore[0], j, i)) {
-      //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+      //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
       queueRowLemma(instore, instore[0], j, i);
     }
   }
@@ -1071,9 +1088,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
 
 
 void TheoryArrays::checkStore(TNode a) {
-  Debug("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
+  Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
 
-  if(Debug.isOn("arrays-cri")) {
+  if(Trace.isOn("arrays-cri")) {
     d_infoMap.getInfo(a)->print();
   }
   Assert(a.getType().isArray());
@@ -1088,7 +1105,7 @@ void TheoryArrays::checkStore(TNode a) {
     TNode j = *it;
 
     if(!isRedundandRowLemma(a, b, i, j)) {
-      //Debug("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
+      //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
       queueRowLemma(a,b,i,j);
     }
   }
@@ -1116,8 +1133,8 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
  Assert(a.getType().isArray());
  Assert(b.getType().isArray());
 
- Debug("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n";
- Debug("arrays-cle")<<"                   and "<<b<<" \n";
+ Trace("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n";
+ Trace("arrays-cle")<<"                   and "<<b<<" \n";
 
 
  if(   d_extAlreadyAdded.count(make_pair(a, b)) == 0
@@ -1131,13 +1148,13 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
    Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk));
    Node lem = nm->mkNode(kind::OR, eq, neq);
 
-   Debug("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n";
+   Trace("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n";
    d_extAlreadyAdded.insert(make_pair(a,b));
    d_out->lemma(lem);
    ++d_numExt;
    return;
  }
- Debug("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
+ Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
 
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index f4cccfec5..cf822cb65 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -260,7 +260,7 @@ private:
 
 
   bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) {
-    //Debug("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+    //Trace("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
     std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin();
     a = find(a);
     b = find(b);
@@ -274,7 +274,7 @@ private:
       TNode i_ = find((*it).third);
       TNode j_ = find((*it).fourth);
       if( a == a_ && b == b_ && i==i_ && j==j_) {
-        //Debug("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
+        //Trace("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
         return true;
       }
     }
@@ -384,25 +384,25 @@ public:
    */
   void preRegisterTerm(TNode n) {
     //TimerStat::CodeTimer codeTimer(d_preregisterTimer);
-    Debug("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n";
+    Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n";
     //TODO: check non-linear arrays with an AlwaysAssert!!!
     //if(n.getType().isArray())
 
     switch(n.getKind()) {
     case kind::EQUAL:
       // stores the seen atoms for propagation
-      Debug("arrays-preregister")<<"atom "<<n<<"\n";
+      Trace("arrays-preregister")<<"atom "<<n<<"\n";
       d_atoms.insert(n);
       // add to proper equality lists
       addEq(n);
       break;
     case kind::SELECT:
-      //Debug("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n";
+      //Trace("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n";
       d_infoMap.addIndex(n[0], n[1]);
       checkRowForIndex(n[1], find(n[0]));
-      //Debug("arrays-preregister")<<"n[0] \n";
+      //Trace("arrays-preregister")<<"n[0] \n";
       //d_infoMap.getInfo(n[0])->print();
-      //Debug("arrays-preregister")<<"find(n[0]) \n";
+      //Trace("arrays-preregister")<<"find(n[0]) \n";
       //d_infoMap.getInfo(find(n[0]))->print();
       break;
 
@@ -428,16 +428,16 @@ public:
       break;
     }
     default:
-      Debug("darrays")<<"Arrays::preRegisterTerm non-array term. \n";
+      Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n";
     }
   }
 
   //void registerTerm(TNode n) {
-  //  Debug("arrays-register")<<"Arrays::registerTerm "<<n<<"\n";
+  //  Trace("arrays-register")<<"Arrays::registerTerm "<<n<<"\n";
   //}
 
   void presolve() {
-    Debug("arrays")<<"Presolving \n";
+    Trace("arrays")<<"Presolving \n";
     d_donePreregister = true;
   }
 
@@ -447,7 +447,7 @@ public:
 
   void propagate(Effort e) {
 
-    Debug("arrays-prop")<<"Propagating \n";
+    Trace("arrays-prop")<<"Propagating \n";
 
     context::CDList<TNode>::const_iterator it = d_prop_queue.begin();
     /*
@@ -466,10 +466,10 @@ public:
     for(; it!= d_atoms.end(); it++) {
       TNode eq = *it;
       Assert(eq.getKind()==kind::EQUAL);
-      Debug("arrays-prop")<<"value of "<<eq<<" ";
-      Debug("arrays-prop")<<d_valuation.getSatValue(eq);
+      Trace("arrays-prop")<<"value of "<<eq<<" ";
+      Trace("arrays-prop")<<d_valuation.getSatValue(eq);
       if(find(eq[0]) == find(eq[1])) {
-        Debug("arrays-prop")<<" eq \n";
+        Trace("arrays-prop")<<" eq \n";
         ++d_numProp;
       }
     }
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 059b7ce8b..d7b37d8ba 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -33,7 +33,7 @@ class TheoryArraysRewriter {
 public:
 
   static RewriteResponse postRewrite(TNode node) {
-    Debug("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
+    Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
     switch (node.getKind()) {
       case kind::SELECT: {
         // select(store(a,i,v),i) = v
@@ -85,7 +85,7 @@ public:
   }
 
   static inline RewriteResponse preRewrite(TNode node) {
-    Debug("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl;
+    Trace("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl;
     return RewriteResponse(REWRITE_DONE, node);
   }
 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index e896f9058..bb42a5ec7 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -64,7 +64,7 @@ Node Rewriter::rewrite(Node node) {
 
 Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
-  Debug("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
+  Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
 
   // Put the node on the stack in order to start the "recursive" rewrite
   vector<RewriteStackElement> rewriteStack;
@@ -76,7 +76,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
     // Get the top of the recursion stack
     RewriteStackElement& rewriteStackTop = rewriteStack.back();
 
-    Debug("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl;
+    Trace("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl;
 
     // Before rewriting children we need to do a pre-rewrite of the node
     if (rewriteStackTop.nextChild == 0) {
diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h
index 86c2585b1..a2b2d06b7 100644
--- a/src/theory/rewriter_attributes.h
+++ b/src/theory/rewriter_attributes.h
@@ -51,7 +51,7 @@ struct RewriteAttibute {
    * Set the value of the pre-rewrite cache.
    */
   static void setPreRewriteCache(TNode node, TNode cache) throw() {
-    Debug("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl;
+    Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl;
     Assert(!cache.isNull());
     if (node == cache) {
       node.setAttribute(pre_rewrite(), Node::null());
@@ -83,7 +83,7 @@ struct RewriteAttibute {
    */
   static void setPostRewriteCache(TNode node, TNode cache) throw() {
     Assert(!cache.isNull());
-    Debug("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl;
+    Trace("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl;
     if (node == cache) {
       node.setAttribute(post_rewrite(), Node::null());
     } else {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 56a5f2f76..93d78f57c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -140,7 +140,7 @@ protected:
     TNode fact = d_facts[d_factsHead];
     d_wasSharedTermFact = false;
     d_factsHead = d_factsHead + 1;
-    Debug("theory") << "Theory::get() => " << fact
+    Trace("theory") << "Theory::get() => " << fact
                     << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
     d_out->newFact(fact);
     return fact;
@@ -312,7 +312,7 @@ public:
    * Assert a fact in the current context.
    */
   void assertFact(TNode node) {
-    Debug("theory") << "Theory::assertFact(" << node << ")" << std::endl;
+    Trace("theory") << "Theory::assertFact(" << node << ")" << std::endl;
     d_facts.push_back(node);
   }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 3571171f8..28d7ab2c0 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -73,7 +73,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
     list<TNode> toReg;
     toReg.push_back(fact);
 
-    Debug("theory") << "Theory::get(): registering new atom" << endl;
+    Trace("theory") << "Theory::get(): registering new atom" << endl;
 
     /* Essentially this is doing a breadth-first numbering of
      * non-registered subterms with children.  Any non-registered
@@ -195,20 +195,20 @@ void TheoryEngine::preRegister(TNode preprocessed) {
           } else {
             Theory* theory = theoryOf(current);
             TheoryId theoryLHS = theory->getId();
-            Debug("register") << "preregistering " << current
+            Trace("register") << "preregistering " << current
                               << " with " << theoryLHS << std::endl;
             markActive(theoryLHS);
             theory->preRegisterTerm(current);
           }
         } else {
           TheoryId theory = theoryIdOf(current);
-          Debug("register") << "preregistering " << current
+          Trace("register") << "preregistering " << current
                             << " with " << theory << std::endl;
           markActive(theory);
           d_theoryTable[theory]->preRegisterTerm(current);
           TheoryId typeTheory = theoryIdOf(current.getType());
           if (theory != typeTheory) {
-            Debug("register") << "preregistering " << current
+            Trace("register") << "preregistering " << current
                               << " with " << typeTheory << std::endl;
             markActive(typeTheory);
             d_theoryTable[typeTheory]->preRegisterTerm(current);
@@ -254,7 +254,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) {
   try {
     CVC4_FOR_EACH_THEORY;
   } catch(const theory::Interrupted&) {
-    Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
+    Trace("theory") << "TheoryEngine::check() => conflict" << std::endl;
   }
 
   return true;
@@ -315,7 +315,7 @@ bool TheoryEngine::presolve() {
     // Presolve for each theory using the statement above
     CVC4_FOR_EACH_THEORY;
   } catch(const theory::Interrupted&) {
-    Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
+    Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
   }
   // return whether we have a conflict
   return !d_theoryOut.d_conflictNode.get().isNull();
@@ -374,9 +374,9 @@ bool TheoryEngine::hasRegisterTerm(TheoryId th) const {
 
 theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) {
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
-  Debug("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl;
+  Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl;
   Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut);
-  Debug("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl;
+  Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl;
   return solveStatus;
 }
 
@@ -390,7 +390,7 @@ struct preprocess_stack_element {
 
 Node TheoryEngine::preprocess(TNode assertion) {
 
-  Debug("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl;
+  Trace("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl;
 
     // Do a topological sort of the subexpressions and substitute them
   vector<preprocess_stack_element> toVisit;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d4138f807..3507723f9 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -126,7 +126,7 @@ class TheoryEngine {
 
     void conflict(TNode conflictNode, bool safe)
       throw(theory::Interrupted, AssertionException) {
-      Debug("theory") << "EngineOutputChannel::conflict("
+      Trace("theory") << "EngineOutputChannel::conflict("
                       << conflictNode << ")" << std::endl;
       d_conflictNode = conflictNode;
       ++(d_engine->d_statistics.d_statConflicts);
@@ -137,7 +137,7 @@ class TheoryEngine {
 
     void propagate(TNode lit, bool)
       throw(theory::Interrupted, AssertionException) {
-      Debug("theory") << "EngineOutputChannel::propagate("
+      Trace("theory") << "EngineOutputChannel::propagate("
                       << lit << ")" << std::endl;
       d_propagatedLiterals.push_back(lit);
       ++(d_engine->d_statistics.d_statPropagate);
@@ -145,7 +145,7 @@ class TheoryEngine {
 
     void lemma(TNode node, bool)
       throw(theory::Interrupted, AssertionException) {
-      Debug("theory") << "EngineOutputChannel::lemma("
+      Trace("theory") << "EngineOutputChannel::lemma("
                       << node << ")" << std::endl;
       ++(d_engine->d_statistics.d_statLemma);
       d_engine->newLemma(node);
@@ -153,7 +153,7 @@ class TheoryEngine {
 
     void explanation(TNode explanationNode, bool)
       throw(theory::Interrupted, AssertionException) {
-      Debug("theory") << "EngineOutputChannel::explanation("
+      Trace("theory") << "EngineOutputChannel::explanation("
                       << explanationNode << ")" << std::endl;
       d_explanationNode = explanationNode;
       ++(d_engine->d_statistics.d_statExplanation);
@@ -355,7 +355,7 @@ public:
    * @param node the assertion
    */
   inline void assertFact(TNode node) {
-    Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
+    Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 
     // Mark it as asserted in this context
     //
@@ -369,16 +369,16 @@ public:
     // Again, equality is a special case
     if (atom.getKind() == kind::EQUAL) {
       if(d_logic == "QF_AX") {
-        Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl;
+        Trace("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl;
         d_theoryTable[theory::THEORY_ARRAY]->assertFact(node);
       } else {
         theory::Theory* theory = theoryOf(atom);
-        Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl;
+        Trace("theory") << "asserting " << node << " to " << theory->getId() << std::endl;
         theory->assertFact(node);
       }
     } else {
       theory::Theory* theory = theoryOf(atom);
-      Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl;
+      Trace("theory") << "asserting " << node << " to " << theory->getId() << std::endl;
       theory->assertFact(node);
     }
   }
@@ -443,7 +443,7 @@ public:
     TNode atom = node.getKind() == kind::NOT ? node[0] : node;
     if (atom.getKind() == kind::EQUAL) {
       if(d_logic == "QF_AX") {
-        Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl;
+        Trace("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl;
         d_theoryTable[theory::THEORY_ARRAY]->explain(node);
       } else {
         theoryOf(atom[0])->explain(node);
diff --git a/test/regress/regress0/arrays/bug272.minimized.smt b/test/regress/regress0/arrays/bug272.minimized.smt
new file mode 100644
index 000000000..360740310
--- /dev/null
+++ b/test/regress/regress0/arrays/bug272.minimized.smt
@@ -0,0 +1,32 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:extrafuns ((v2 Index))
+:extrafuns ((v0 Array))
+:extrafuns ((v3 Element))
+:extrafuns ((v1 Index))
+:status sat
+:formula
+(flet ($n1 true)
+(let (?n2 (select v0 v2))
+(flet ($n3 (= v3 ?n2))
+(let (?n4 (store v0 v1 v3))
+(let (?n5 (store ?n4 v2 v3))
+(let (?n6 (store ?n4 v2 ?n2))
+(flet ($n7 (= ?n5 ?n6))
+(let (?n8 (store ?n5 v1 ?n2))
+(let (?n9 (ite $n7 ?n5 ?n8))
+(flet ($n10 (= v0 ?n6))
+(flet ($n11 (distinct ?n5 ?n8))
+(let (?n12 (select ?n5 v1))
+(flet ($n13 (distinct v3 ?n12))
+(let (?n14 (ite $n13 v3 ?n12))
+(let (?n15 (ite $n11 v3 ?n14))
+(flet ($n16 (= ?n4 ?n6))
+(let (?n17 (ite $n16 ?n2 ?n2))
+(let (?n18 (ite $n10 ?n15 ?n17))
+(let (?n19 (store ?n5 v1 ?n18))
+(flet ($n20 (distinct ?n9 ?n19))
+(flet ($n21 (or $n3 $n20))
+(flet ($n22 (xor $n1 $n21))
+$n22
+)))))))))))))))))))))))
diff --git a/test/regress/regress0/arrays/bug272.smt b/test/regress/regress0/arrays/bug272.smt
new file mode 100644
index 000000000..c7e779acd
--- /dev/null
+++ b/test/regress/regress0/arrays/bug272.smt
@@ -0,0 +1,312 @@
+(benchmark fuzzsmt
+:logic QF_AX
+:status sat
+:extrafuns ((v0 Array))
+:extrafuns ((v1 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Element))
+:formula
+(let (?e4 (store v0 v1 v3))
+(let (?e5 (store ?e4 v2 v3))
+(let (?e6 (store ?e4 v2 v3))
+(let (?e7 (select v0 v2))
+(let (?e8 (store ?e6 v1 ?e7))
+(let (?e9 (select ?e6 v1))
+(let (?e10 (store ?e4 v2 ?e7))
+(flet ($e11 (distinct v0 ?e6))
+(flet ($e12 (distinct ?e6 ?e5))
+(flet ($e13 (distinct ?e8 ?e6))
+(flet ($e14 (= ?e10 v0))
+(flet ($e15 (= ?e10 ?e6))
+(flet ($e16 (distinct ?e6 ?e6))
+(flet ($e17 (= v0 ?e10))
+(flet ($e18 (= ?e4 ?e10))
+(flet ($e19 (distinct v2 v2))
+(flet ($e20 (distinct v2 v2))
+(flet ($e21 (= v1 v2))
+(flet ($e22 (distinct v3 ?e7))
+(flet ($e23 (distinct ?e9 v3))
+(let (?e24 (ite $e21 ?e4 ?e8))
+(let (?e25 (ite $e22 ?e5 ?e8))
+(let (?e26 (ite $e20 ?e24 ?e6))
+(let (?e27 (ite $e15 ?e6 ?e10))
+(let (?e28 (ite $e23 ?e10 ?e27))
+(let (?e29 (ite $e11 v0 ?e28))
+(let (?e30 (ite $e15 ?e25 ?e8))
+(let (?e31 (ite $e18 ?e4 ?e25))
+(let (?e32 (ite $e23 ?e31 ?e26))
+(let (?e33 (ite $e14 ?e6 ?e32))
+(let (?e34 (ite $e16 ?e31 ?e33))
+(let (?e35 (ite $e19 ?e10 ?e29))
+(let (?e36 (ite $e17 v0 ?e6))
+(let (?e37 (ite $e13 ?e36 ?e32))
+(let (?e38 (ite $e20 ?e26 ?e27))
+(let (?e39 (ite $e12 ?e29 ?e25))
+(let (?e40 (ite $e15 v1 v1))
+(let (?e41 (ite $e21 ?e40 v2))
+(let (?e42 (ite $e17 v1 v1))
+(let (?e43 (ite $e13 ?e42 ?e42))
+(let (?e44 (ite $e20 ?e41 ?e40))
+(let (?e45 (ite $e22 ?e40 ?e43))
+(let (?e46 (ite $e19 ?e41 ?e45))
+(let (?e47 (ite $e21 v2 ?e42))
+(let (?e48 (ite $e11 v2 v2))
+(let (?e49 (ite $e13 ?e43 ?e45))
+(let (?e50 (ite $e20 ?e45 v1))
+(let (?e51 (ite $e12 v1 ?e46))
+(let (?e52 (ite $e15 ?e41 ?e49))
+(let (?e53 (ite $e23 ?e44 ?e48))
+(let (?e54 (ite $e20 ?e48 ?e52))
+(let (?e55 (ite $e17 ?e50 v2))
+(let (?e56 (ite $e16 ?e46 v2))
+(let (?e57 (ite $e18 ?e55 ?e52))
+(let (?e58 (ite $e14 ?e43 ?e53))
+(let (?e59 (ite $e18 ?e7 ?e7))
+(let (?e60 (ite $e19 v3 v3))
+(let (?e61 (ite $e14 ?e59 ?e60))
+(let (?e62 (ite $e23 v3 ?e9))
+(let (?e63 (ite $e22 ?e59 ?e59))
+(let (?e64 (ite $e13 ?e62 ?e61))
+(let (?e65 (ite $e15 ?e7 ?e9))
+(let (?e66 (ite $e13 ?e60 ?e62))
+(let (?e67 (ite $e21 ?e62 ?e65))
+(let (?e68 (ite $e20 ?e60 ?e62))
+(let (?e69 (ite $e12 ?e64 ?e9))
+(let (?e70 (ite $e16 v3 ?e68))
+(let (?e71 (ite $e14 ?e62 ?e64))
+(let (?e72 (ite $e16 ?e60 ?e62))
+(let (?e73 (ite $e11 ?e7 ?e63))
+(let (?e74 (ite $e17 ?e66 ?e59))
+(let (?e75 (store ?e36 ?e51 ?e70))
+(let (?e76 (store ?e26 ?e43 ?e74))
+(let (?e77 (store ?e76 ?e50 ?e7))
+(let (?e78 (select ?e31 ?e44))
+(let (?e79 (select v0 ?e40))
+(let (?e80 (store ?e33 ?e48 ?e7))
+(let (?e81 (select ?e39 ?e57))
+(let (?e82 (store ?e26 ?e57 ?e81))
+(flet ($e83 (= ?e35 ?e31))
+(flet ($e84 (= ?e28 ?e4))
+(flet ($e85 (= ?e75 ?e80))
+(flet ($e86 (distinct ?e37 ?e30))
+(flet ($e87 (= ?e39 ?e39))
+(flet ($e88 (= ?e30 ?e82))
+(flet ($e89 (distinct ?e26 ?e31))
+(flet ($e90 (= ?e31 ?e8))
+(flet ($e91 (= ?e33 ?e76))
+(flet ($e92 (distinct ?e77 ?e27))
+(flet ($e93 (= ?e32 ?e38))
+(flet ($e94 (= ?e75 ?e82))
+(flet ($e95 (distinct ?e39 ?e75))
+(flet ($e96 (= ?e30 ?e82))
+(flet ($e97 (distinct ?e39 ?e33))
+(flet ($e98 (= ?e32 ?e6))
+(flet ($e99 (distinct ?e35 ?e4))
+(flet ($e100 (distinct ?e6 ?e75))
+(flet ($e101 (distinct ?e76 v0))
+(flet ($e102 (distinct ?e76 ?e76))
+(flet ($e103 (distinct ?e76 ?e30))
+(flet ($e104 (distinct ?e25 ?e35))
+(flet ($e105 (= ?e39 ?e8))
+(flet ($e106 (distinct ?e38 ?e26))
+(flet ($e107 (distinct ?e10 ?e4))
+(flet ($e108 (= ?e24 ?e82))
+(flet ($e109 (= ?e30 ?e24))
+(flet ($e110 (= ?e5 ?e5))
+(flet ($e111 (distinct ?e82 ?e80))
+(flet ($e112 (= ?e36 ?e26))
+(flet ($e113 (distinct ?e82 ?e6))
+(flet ($e114 (= ?e4 ?e80))
+(flet ($e115 (distinct ?e80 ?e32))
+(flet ($e116 (= ?e37 ?e4))
+(flet ($e117 (distinct ?e24 ?e29))
+(flet ($e118 (= ?e80 ?e10))
+(flet ($e119 (distinct ?e24 ?e34))
+(flet ($e120 (= ?e49 ?e43))
+(flet ($e121 (distinct ?e54 ?e41))
+(flet ($e122 (= ?e46 ?e45))
+(flet ($e123 (distinct v2 v2))
+(flet ($e124 (distinct v1 ?e58))
+(flet ($e125 (distinct ?e56 ?e45))
+(flet ($e126 (= ?e48 ?e47))
+(flet ($e127 (distinct ?e46 ?e43))
+(flet ($e128 (distinct ?e58 ?e43))
+(flet ($e129 (= ?e58 ?e47))
+(flet ($e130 (distinct ?e50 ?e40))
+(flet ($e131 (= ?e44 ?e42))
+(flet ($e132 (= v2 ?e46))
+(flet ($e133 (distinct ?e50 ?e53))
+(flet ($e134 (distinct ?e42 ?e54))
+(flet ($e135 (= ?e53 ?e58))
+(flet ($e136 (distinct v1 ?e52))
+(flet ($e137 (distinct ?e58 ?e53))
+(flet ($e138 (distinct v1 ?e54))
+(flet ($e139 (= ?e47 ?e43))
+(flet ($e140 (= ?e44 ?e41))
+(flet ($e141 (= ?e44 ?e40))
+(flet ($e142 (distinct ?e50 ?e55))
+(flet ($e143 (= ?e52 ?e40))
+(flet ($e144 (= ?e56 ?e43))
+(flet ($e145 (= ?e44 ?e48))
+(flet ($e146 (distinct ?e42 ?e51))
+(flet ($e147 (= ?e56 v2))
+(flet ($e148 (= ?e56 ?e57))
+(flet ($e149 (= ?e61 ?e73))
+(flet ($e150 (distinct ?e73 v3))
+(flet ($e151 (distinct ?e69 ?e70))
+(flet ($e152 (= ?e59 ?e63))
+(flet ($e153 (= ?e9 ?e65))
+(flet ($e154 (= ?e71 ?e64))
+(flet ($e155 (distinct ?e69 ?e73))
+(flet ($e156 (distinct ?e71 ?e78))
+(flet ($e157 (distinct ?e63 ?e78))
+(flet ($e158 (distinct ?e7 ?e66))
+(flet ($e159 (= ?e7 ?e62))
+(flet ($e160 (= ?e81 ?e65))
+(flet ($e161 (= ?e73 ?e63))
+(flet ($e162 (distinct ?e72 ?e73))
+(flet ($e163 (= v3 ?e68))
+(flet ($e164 (= ?e72 ?e73))
+(flet ($e165 (= ?e73 ?e60))
+(flet ($e166 (= ?e73 v3))
+(flet ($e167 (= ?e63 ?e73))
+(flet ($e168 (= v3 ?e59))
+(flet ($e169 (distinct ?e68 ?e67))
+(flet ($e170 (distinct ?e63 ?e66))
+(flet ($e171 (distinct ?e72 ?e64))
+(flet ($e172 (= ?e72 ?e65))
+(flet ($e173 (= ?e72 ?e7))
+(flet ($e174 (distinct ?e67 ?e62))
+(flet ($e175 (distinct ?e66 ?e72))
+(flet ($e176 (distinct ?e68 ?e79))
+(flet ($e177 (distinct ?e70 ?e63))
+(flet ($e178 (distinct ?e9 ?e73))
+(flet ($e179 (distinct ?e7 ?e60))
+(flet ($e180 (= ?e66 ?e71))
+(flet ($e181 (distinct ?e63 ?e63))
+(flet ($e182 (distinct ?e9 ?e74))
+(flet ($e183 (implies $e123 $e123))
+(flet ($e184 (iff $e148 $e146))
+(flet ($e185 (or $e91 $e160))
+(flet ($e186 (xor $e95 $e100))
+(flet ($e187 (not $e164))
+(flet ($e188 (iff $e135 $e128))
+(flet ($e189 (iff $e11 $e153))
+(flet ($e190 (iff $e16 $e151))
+(flet ($e191 (not $e23))
+(flet ($e192 (and $e90 $e84))
+(flet ($e193 (or $e161 $e145))
+(flet ($e194 (implies $e112 $e129))
+(flet ($e195 (iff $e102 $e109))
+(flet ($e196 (or $e188 $e124))
+(flet ($e197 (implies $e21 $e87))
+(flet ($e198 (not $e12))
+(flet ($e199 (and $e139 $e173))
+(flet ($e200 (if_then_else $e85 $e108 $e169))
+(flet ($e201 (implies $e152 $e88))
+(flet ($e202 (iff $e105 $e178))
+(flet ($e203 (xor $e133 $e162))
+(flet ($e204 (or $e167 $e154))
+(flet ($e205 (or $e150 $e194))
+(flet ($e206 (not $e119))
+(flet ($e207 (if_then_else $e184 $e199 $e17))
+(flet ($e208 (xor $e200 $e141))
+(flet ($e209 (not $e185))
+(flet ($e210 (not $e176))
+(flet ($e211 (or $e210 $e177))
+(flet ($e212 (or $e97 $e193))
+(flet ($e213 (iff $e92 $e158))
+(flet ($e214 (if_then_else $e204 $e180 $e174))
+(flet ($e215 (or $e103 $e165))
+(flet ($e216 (and $e116 $e138))
+(flet ($e217 (not $e168))
+(flet ($e218 (implies $e157 $e106))
+(flet ($e219 (or $e93 $e182))
+(flet ($e220 (xor $e203 $e186))
+(flet ($e221 (implies $e122 $e83))
+(flet ($e222 (implies $e137 $e14))
+(flet ($e223 (xor $e192 $e94))
+(flet ($e224 (if_then_else $e89 $e207 $e111))
+(flet ($e225 (if_then_else $e127 $e224 $e15))
+(flet ($e226 (implies $e22 $e212))
+(flet ($e227 (or $e110 $e125))
+(flet ($e228 (not $e104))
+(flet ($e229 (not $e209))
+(flet ($e230 (and $e172 $e214))
+(flet ($e231 (not $e101))
+(flet ($e232 (not $e126))
+(flet ($e233 (not $e196))
+(flet ($e234 (or $e228 $e86))
+(flet ($e235 (xor $e201 $e18))
+(flet ($e236 (if_then_else $e223 $e231 $e147))
+(flet ($e237 (implies $e144 $e208))
+(flet ($e238 (not $e175))
+(flet ($e239 (if_then_else $e211 $e225 $e159))
+(flet ($e240 (or $e190 $e156))
+(flet ($e241 (not $e233))
+(flet ($e242 (if_then_else $e220 $e170 $e205))
+(flet ($e243 (xor $e238 $e136))
+(flet ($e244 (and $e149 $e163))
+(flet ($e245 (and $e206 $e155))
+(flet ($e246 (and $e219 $e187))
+(flet ($e247 (and $e235 $e227))
+(flet ($e248 (iff $e222 $e239))
+(flet ($e249 (implies $e179 $e195))
+(flet ($e250 (not $e191))
+(flet ($e251 (or $e249 $e197))
+(flet ($e252 (xor $e221 $e242))
+(flet ($e253 (if_then_else $e130 $e240 $e202))
+(flet ($e254 (not $e244))
+(flet ($e255 (and $e230 $e120))
+(flet ($e256 (iff $e189 $e140))
+(flet ($e257 (implies $e213 $e19))
+(flet ($e258 (and $e96 $e252))
+(flet ($e259 (and $e256 $e257))
+(flet ($e260 (xor $e259 $e134))
+(flet ($e261 (not $e166))
+(flet ($e262 (implies $e216 $e181))
+(flet ($e263 (not $e260))
+(flet ($e264 (xor $e258 $e142))
+(flet ($e265 (if_then_else $e131 $e229 $e13))
+(flet ($e266 (not $e143))
+(flet ($e267 (or $e237 $e262))
+(flet ($e268 (if_then_else $e267 $e245 $e248))
+(flet ($e269 (implies $e171 $e254))
+(flet ($e270 (if_then_else $e243 $e269 $e268))
+(flet ($e271 (xor $e250 $e265))
+(flet ($e272 (implies $e121 $e253))
+(flet ($e273 (not $e113))
+(flet ($e274 (and $e232 $e198))
+(flet ($e275 (implies $e99 $e263))
+(flet ($e276 (implies $e117 $e275))
+(flet ($e277 (or $e270 $e114))
+(flet ($e278 (or $e246 $e247))
+(flet ($e279 (and $e255 $e241))
+(flet ($e280 (not $e278))
+(flet ($e281 (and $e217 $e280))
+(flet ($e282 (if_then_else $e277 $e251 $e251))
+(flet ($e283 (or $e274 $e282))
+(flet ($e284 (and $e98 $e236))
+(flet ($e285 (or $e271 $e115))
+(flet ($e286 (or $e272 $e284))
+(flet ($e287 (not $e279))
+(flet ($e288 (implies $e283 $e273))
+(flet ($e289 (not $e20))
+(flet ($e290 (or $e289 $e286))
+(flet ($e291 (if_then_else $e276 $e226 $e118))
+(flet ($e292 (and $e285 $e266))
+(flet ($e293 (xor $e218 $e218))
+(flet ($e294 (iff $e292 $e281))
+(flet ($e295 (if_then_else $e293 $e183 $e234))
+(flet ($e296 (or $e132 $e295))
+(flet ($e297 (xor $e288 $e261))
+(flet ($e298 (xor $e294 $e107))
+(flet ($e299 (and $e290 $e215))
+(flet ($e300 (and $e297 $e264))
+(flet ($e301 (or $e300 $e287))
+(flet ($e302 (or $e296 $e298))
+(flet ($e303 (xor $e291 $e299))
+(flet ($e304 (if_then_else $e302 $e303 $e301))
+$e304
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/arrays/unsound1.minimized.smt b/test/regress/regress0/arrays/unsound1.minimized.smt
deleted file mode 100644
index 360740310..000000000
--- a/test/regress/regress0/arrays/unsound1.minimized.smt
+++ /dev/null
@@ -1,32 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_AX
-:extrafuns ((v2 Index))
-:extrafuns ((v0 Array))
-:extrafuns ((v3 Element))
-:extrafuns ((v1 Index))
-:status sat
-:formula
-(flet ($n1 true)
-(let (?n2 (select v0 v2))
-(flet ($n3 (= v3 ?n2))
-(let (?n4 (store v0 v1 v3))
-(let (?n5 (store ?n4 v2 v3))
-(let (?n6 (store ?n4 v2 ?n2))
-(flet ($n7 (= ?n5 ?n6))
-(let (?n8 (store ?n5 v1 ?n2))
-(let (?n9 (ite $n7 ?n5 ?n8))
-(flet ($n10 (= v0 ?n6))
-(flet ($n11 (distinct ?n5 ?n8))
-(let (?n12 (select ?n5 v1))
-(flet ($n13 (distinct v3 ?n12))
-(let (?n14 (ite $n13 v3 ?n12))
-(let (?n15 (ite $n11 v3 ?n14))
-(flet ($n16 (= ?n4 ?n6))
-(let (?n17 (ite $n16 ?n2 ?n2))
-(let (?n18 (ite $n10 ?n15 ?n17))
-(let (?n19 (store ?n5 v1 ?n18))
-(flet ($n20 (distinct ?n9 ?n19))
-(flet ($n21 (or $n3 $n20))
-(flet ($n22 (xor $n1 $n21))
-$n22
-)))))))))))))))))))))))
diff --git a/test/regress/regress0/arrays/unsound1.smt b/test/regress/regress0/arrays/unsound1.smt
deleted file mode 100644
index c7e779acd..000000000
--- a/test/regress/regress0/arrays/unsound1.smt
+++ /dev/null
@@ -1,312 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_AX
-:status sat
-:extrafuns ((v0 Array))
-:extrafuns ((v1 Index))
-:extrafuns ((v2 Index))
-:extrafuns ((v3 Element))
-:formula
-(let (?e4 (store v0 v1 v3))
-(let (?e5 (store ?e4 v2 v3))
-(let (?e6 (store ?e4 v2 v3))
-(let (?e7 (select v0 v2))
-(let (?e8 (store ?e6 v1 ?e7))
-(let (?e9 (select ?e6 v1))
-(let (?e10 (store ?e4 v2 ?e7))
-(flet ($e11 (distinct v0 ?e6))
-(flet ($e12 (distinct ?e6 ?e5))
-(flet ($e13 (distinct ?e8 ?e6))
-(flet ($e14 (= ?e10 v0))
-(flet ($e15 (= ?e10 ?e6))
-(flet ($e16 (distinct ?e6 ?e6))
-(flet ($e17 (= v0 ?e10))
-(flet ($e18 (= ?e4 ?e10))
-(flet ($e19 (distinct v2 v2))
-(flet ($e20 (distinct v2 v2))
-(flet ($e21 (= v1 v2))
-(flet ($e22 (distinct v3 ?e7))
-(flet ($e23 (distinct ?e9 v3))
-(let (?e24 (ite $e21 ?e4 ?e8))
-(let (?e25 (ite $e22 ?e5 ?e8))
-(let (?e26 (ite $e20 ?e24 ?e6))
-(let (?e27 (ite $e15 ?e6 ?e10))
-(let (?e28 (ite $e23 ?e10 ?e27))
-(let (?e29 (ite $e11 v0 ?e28))
-(let (?e30 (ite $e15 ?e25 ?e8))
-(let (?e31 (ite $e18 ?e4 ?e25))
-(let (?e32 (ite $e23 ?e31 ?e26))
-(let (?e33 (ite $e14 ?e6 ?e32))
-(let (?e34 (ite $e16 ?e31 ?e33))
-(let (?e35 (ite $e19 ?e10 ?e29))
-(let (?e36 (ite $e17 v0 ?e6))
-(let (?e37 (ite $e13 ?e36 ?e32))
-(let (?e38 (ite $e20 ?e26 ?e27))
-(let (?e39 (ite $e12 ?e29 ?e25))
-(let (?e40 (ite $e15 v1 v1))
-(let (?e41 (ite $e21 ?e40 v2))
-(let (?e42 (ite $e17 v1 v1))
-(let (?e43 (ite $e13 ?e42 ?e42))
-(let (?e44 (ite $e20 ?e41 ?e40))
-(let (?e45 (ite $e22 ?e40 ?e43))
-(let (?e46 (ite $e19 ?e41 ?e45))
-(let (?e47 (ite $e21 v2 ?e42))
-(let (?e48 (ite $e11 v2 v2))
-(let (?e49 (ite $e13 ?e43 ?e45))
-(let (?e50 (ite $e20 ?e45 v1))
-(let (?e51 (ite $e12 v1 ?e46))
-(let (?e52 (ite $e15 ?e41 ?e49))
-(let (?e53 (ite $e23 ?e44 ?e48))
-(let (?e54 (ite $e20 ?e48 ?e52))
-(let (?e55 (ite $e17 ?e50 v2))
-(let (?e56 (ite $e16 ?e46 v2))
-(let (?e57 (ite $e18 ?e55 ?e52))
-(let (?e58 (ite $e14 ?e43 ?e53))
-(let (?e59 (ite $e18 ?e7 ?e7))
-(let (?e60 (ite $e19 v3 v3))
-(let (?e61 (ite $e14 ?e59 ?e60))
-(let (?e62 (ite $e23 v3 ?e9))
-(let (?e63 (ite $e22 ?e59 ?e59))
-(let (?e64 (ite $e13 ?e62 ?e61))
-(let (?e65 (ite $e15 ?e7 ?e9))
-(let (?e66 (ite $e13 ?e60 ?e62))
-(let (?e67 (ite $e21 ?e62 ?e65))
-(let (?e68 (ite $e20 ?e60 ?e62))
-(let (?e69 (ite $e12 ?e64 ?e9))
-(let (?e70 (ite $e16 v3 ?e68))
-(let (?e71 (ite $e14 ?e62 ?e64))
-(let (?e72 (ite $e16 ?e60 ?e62))
-(let (?e73 (ite $e11 ?e7 ?e63))
-(let (?e74 (ite $e17 ?e66 ?e59))
-(let (?e75 (store ?e36 ?e51 ?e70))
-(let (?e76 (store ?e26 ?e43 ?e74))
-(let (?e77 (store ?e76 ?e50 ?e7))
-(let (?e78 (select ?e31 ?e44))
-(let (?e79 (select v0 ?e40))
-(let (?e80 (store ?e33 ?e48 ?e7))
-(let (?e81 (select ?e39 ?e57))
-(let (?e82 (store ?e26 ?e57 ?e81))
-(flet ($e83 (= ?e35 ?e31))
-(flet ($e84 (= ?e28 ?e4))
-(flet ($e85 (= ?e75 ?e80))
-(flet ($e86 (distinct ?e37 ?e30))
-(flet ($e87 (= ?e39 ?e39))
-(flet ($e88 (= ?e30 ?e82))
-(flet ($e89 (distinct ?e26 ?e31))
-(flet ($e90 (= ?e31 ?e8))
-(flet ($e91 (= ?e33 ?e76))
-(flet ($e92 (distinct ?e77 ?e27))
-(flet ($e93 (= ?e32 ?e38))
-(flet ($e94 (= ?e75 ?e82))
-(flet ($e95 (distinct ?e39 ?e75))
-(flet ($e96 (= ?e30 ?e82))
-(flet ($e97 (distinct ?e39 ?e33))
-(flet ($e98 (= ?e32 ?e6))
-(flet ($e99 (distinct ?e35 ?e4))
-(flet ($e100 (distinct ?e6 ?e75))
-(flet ($e101 (distinct ?e76 v0))
-(flet ($e102 (distinct ?e76 ?e76))
-(flet ($e103 (distinct ?e76 ?e30))
-(flet ($e104 (distinct ?e25 ?e35))
-(flet ($e105 (= ?e39 ?e8))
-(flet ($e106 (distinct ?e38 ?e26))
-(flet ($e107 (distinct ?e10 ?e4))
-(flet ($e108 (= ?e24 ?e82))
-(flet ($e109 (= ?e30 ?e24))
-(flet ($e110 (= ?e5 ?e5))
-(flet ($e111 (distinct ?e82 ?e80))
-(flet ($e112 (= ?e36 ?e26))
-(flet ($e113 (distinct ?e82 ?e6))
-(flet ($e114 (= ?e4 ?e80))
-(flet ($e115 (distinct ?e80 ?e32))
-(flet ($e116 (= ?e37 ?e4))
-(flet ($e117 (distinct ?e24 ?e29))
-(flet ($e118 (= ?e80 ?e10))
-(flet ($e119 (distinct ?e24 ?e34))
-(flet ($e120 (= ?e49 ?e43))
-(flet ($e121 (distinct ?e54 ?e41))
-(flet ($e122 (= ?e46 ?e45))
-(flet ($e123 (distinct v2 v2))
-(flet ($e124 (distinct v1 ?e58))
-(flet ($e125 (distinct ?e56 ?e45))
-(flet ($e126 (= ?e48 ?e47))
-(flet ($e127 (distinct ?e46 ?e43))
-(flet ($e128 (distinct ?e58 ?e43))
-(flet ($e129 (= ?e58 ?e47))
-(flet ($e130 (distinct ?e50 ?e40))
-(flet ($e131 (= ?e44 ?e42))
-(flet ($e132 (= v2 ?e46))
-(flet ($e133 (distinct ?e50 ?e53))
-(flet ($e134 (distinct ?e42 ?e54))
-(flet ($e135 (= ?e53 ?e58))
-(flet ($e136 (distinct v1 ?e52))
-(flet ($e137 (distinct ?e58 ?e53))
-(flet ($e138 (distinct v1 ?e54))
-(flet ($e139 (= ?e47 ?e43))
-(flet ($e140 (= ?e44 ?e41))
-(flet ($e141 (= ?e44 ?e40))
-(flet ($e142 (distinct ?e50 ?e55))
-(flet ($e143 (= ?e52 ?e40))
-(flet ($e144 (= ?e56 ?e43))
-(flet ($e145 (= ?e44 ?e48))
-(flet ($e146 (distinct ?e42 ?e51))
-(flet ($e147 (= ?e56 v2))
-(flet ($e148 (= ?e56 ?e57))
-(flet ($e149 (= ?e61 ?e73))
-(flet ($e150 (distinct ?e73 v3))
-(flet ($e151 (distinct ?e69 ?e70))
-(flet ($e152 (= ?e59 ?e63))
-(flet ($e153 (= ?e9 ?e65))
-(flet ($e154 (= ?e71 ?e64))
-(flet ($e155 (distinct ?e69 ?e73))
-(flet ($e156 (distinct ?e71 ?e78))
-(flet ($e157 (distinct ?e63 ?e78))
-(flet ($e158 (distinct ?e7 ?e66))
-(flet ($e159 (= ?e7 ?e62))
-(flet ($e160 (= ?e81 ?e65))
-(flet ($e161 (= ?e73 ?e63))
-(flet ($e162 (distinct ?e72 ?e73))
-(flet ($e163 (= v3 ?e68))
-(flet ($e164 (= ?e72 ?e73))
-(flet ($e165 (= ?e73 ?e60))
-(flet ($e166 (= ?e73 v3))
-(flet ($e167 (= ?e63 ?e73))
-(flet ($e168 (= v3 ?e59))
-(flet ($e169 (distinct ?e68 ?e67))
-(flet ($e170 (distinct ?e63 ?e66))
-(flet ($e171 (distinct ?e72 ?e64))
-(flet ($e172 (= ?e72 ?e65))
-(flet ($e173 (= ?e72 ?e7))
-(flet ($e174 (distinct ?e67 ?e62))
-(flet ($e175 (distinct ?e66 ?e72))
-(flet ($e176 (distinct ?e68 ?e79))
-(flet ($e177 (distinct ?e70 ?e63))
-(flet ($e178 (distinct ?e9 ?e73))
-(flet ($e179 (distinct ?e7 ?e60))
-(flet ($e180 (= ?e66 ?e71))
-(flet ($e181 (distinct ?e63 ?e63))
-(flet ($e182 (distinct ?e9 ?e74))
-(flet ($e183 (implies $e123 $e123))
-(flet ($e184 (iff $e148 $e146))
-(flet ($e185 (or $e91 $e160))
-(flet ($e186 (xor $e95 $e100))
-(flet ($e187 (not $e164))
-(flet ($e188 (iff $e135 $e128))
-(flet ($e189 (iff $e11 $e153))
-(flet ($e190 (iff $e16 $e151))
-(flet ($e191 (not $e23))
-(flet ($e192 (and $e90 $e84))
-(flet ($e193 (or $e161 $e145))
-(flet ($e194 (implies $e112 $e129))
-(flet ($e195 (iff $e102 $e109))
-(flet ($e196 (or $e188 $e124))
-(flet ($e197 (implies $e21 $e87))
-(flet ($e198 (not $e12))
-(flet ($e199 (and $e139 $e173))
-(flet ($e200 (if_then_else $e85 $e108 $e169))
-(flet ($e201 (implies $e152 $e88))
-(flet ($e202 (iff $e105 $e178))
-(flet ($e203 (xor $e133 $e162))
-(flet ($e204 (or $e167 $e154))
-(flet ($e205 (or $e150 $e194))
-(flet ($e206 (not $e119))
-(flet ($e207 (if_then_else $e184 $e199 $e17))
-(flet ($e208 (xor $e200 $e141))
-(flet ($e209 (not $e185))
-(flet ($e210 (not $e176))
-(flet ($e211 (or $e210 $e177))
-(flet ($e212 (or $e97 $e193))
-(flet ($e213 (iff $e92 $e158))
-(flet ($e214 (if_then_else $e204 $e180 $e174))
-(flet ($e215 (or $e103 $e165))
-(flet ($e216 (and $e116 $e138))
-(flet ($e217 (not $e168))
-(flet ($e218 (implies $e157 $e106))
-(flet ($e219 (or $e93 $e182))
-(flet ($e220 (xor $e203 $e186))
-(flet ($e221 (implies $e122 $e83))
-(flet ($e222 (implies $e137 $e14))
-(flet ($e223 (xor $e192 $e94))
-(flet ($e224 (if_then_else $e89 $e207 $e111))
-(flet ($e225 (if_then_else $e127 $e224 $e15))
-(flet ($e226 (implies $e22 $e212))
-(flet ($e227 (or $e110 $e125))
-(flet ($e228 (not $e104))
-(flet ($e229 (not $e209))
-(flet ($e230 (and $e172 $e214))
-(flet ($e231 (not $e101))
-(flet ($e232 (not $e126))
-(flet ($e233 (not $e196))
-(flet ($e234 (or $e228 $e86))
-(flet ($e235 (xor $e201 $e18))
-(flet ($e236 (if_then_else $e223 $e231 $e147))
-(flet ($e237 (implies $e144 $e208))
-(flet ($e238 (not $e175))
-(flet ($e239 (if_then_else $e211 $e225 $e159))
-(flet ($e240 (or $e190 $e156))
-(flet ($e241 (not $e233))
-(flet ($e242 (if_then_else $e220 $e170 $e205))
-(flet ($e243 (xor $e238 $e136))
-(flet ($e244 (and $e149 $e163))
-(flet ($e245 (and $e206 $e155))
-(flet ($e246 (and $e219 $e187))
-(flet ($e247 (and $e235 $e227))
-(flet ($e248 (iff $e222 $e239))
-(flet ($e249 (implies $e179 $e195))
-(flet ($e250 (not $e191))
-(flet ($e251 (or $e249 $e197))
-(flet ($e252 (xor $e221 $e242))
-(flet ($e253 (if_then_else $e130 $e240 $e202))
-(flet ($e254 (not $e244))
-(flet ($e255 (and $e230 $e120))
-(flet ($e256 (iff $e189 $e140))
-(flet ($e257 (implies $e213 $e19))
-(flet ($e258 (and $e96 $e252))
-(flet ($e259 (and $e256 $e257))
-(flet ($e260 (xor $e259 $e134))
-(flet ($e261 (not $e166))
-(flet ($e262 (implies $e216 $e181))
-(flet ($e263 (not $e260))
-(flet ($e264 (xor $e258 $e142))
-(flet ($e265 (if_then_else $e131 $e229 $e13))
-(flet ($e266 (not $e143))
-(flet ($e267 (or $e237 $e262))
-(flet ($e268 (if_then_else $e267 $e245 $e248))
-(flet ($e269 (implies $e171 $e254))
-(flet ($e270 (if_then_else $e243 $e269 $e268))
-(flet ($e271 (xor $e250 $e265))
-(flet ($e272 (implies $e121 $e253))
-(flet ($e273 (not $e113))
-(flet ($e274 (and $e232 $e198))
-(flet ($e275 (implies $e99 $e263))
-(flet ($e276 (implies $e117 $e275))
-(flet ($e277 (or $e270 $e114))
-(flet ($e278 (or $e246 $e247))
-(flet ($e279 (and $e255 $e241))
-(flet ($e280 (not $e278))
-(flet ($e281 (and $e217 $e280))
-(flet ($e282 (if_then_else $e277 $e251 $e251))
-(flet ($e283 (or $e274 $e282))
-(flet ($e284 (and $e98 $e236))
-(flet ($e285 (or $e271 $e115))
-(flet ($e286 (or $e272 $e284))
-(flet ($e287 (not $e279))
-(flet ($e288 (implies $e283 $e273))
-(flet ($e289 (not $e20))
-(flet ($e290 (or $e289 $e286))
-(flet ($e291 (if_then_else $e276 $e226 $e118))
-(flet ($e292 (and $e285 $e266))
-(flet ($e293 (xor $e218 $e218))
-(flet ($e294 (iff $e292 $e281))
-(flet ($e295 (if_then_else $e293 $e183 $e234))
-(flet ($e296 (or $e132 $e295))
-(flet ($e297 (xor $e288 $e261))
-(flet ($e298 (xor $e294 $e107))
-(flet ($e299 (and $e290 $e215))
-(flet ($e300 (and $e297 $e264))
-(flet ($e301 (or $e300 $e287))
-(flet ($e302 (or $e296 $e298))
-(flet ($e303 (xor $e291 $e299))
-(flet ($e304 (if_then_else $e302 $e303 $e301))
-$e304
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-