Fix term database for non-equal, congruent terms in master equality engine. Disable ITE terms in quant conflict find.

8 files changed, 109 insertions, 81 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ff0da13e1..e44a322b5 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -411,6 +411,11 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
           Node r = fm->getUsedRepresentative(n);
           Trace("fmc-model-debug") << n << " -> " << r << std::endl;
           //AlwaysAssert( fm->areEqual( fm->d_uf_terms[op][i], r ) );
+        }else{
+          if( Trace.isOn("fmc-model-debug") ){
+            Node r = fm->getUsedRepresentative(n);
+            Trace("fmc-model-debug") << "[redundant] " << n << " -> " << r << std::endl;
+          }
         }
       }
       Trace("fmc-model-debug") << std::endl;
@@ -614,7 +619,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
 
         //consider all entries going to non-true
         for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
-          if( d_quant_models[f].d_value[i]!=d_true) {
+          if( d_quant_models[f].d_value[i]!=d_true ) {
             Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
             bool hasStar = false;
             std::vector< Node > inst;
@@ -684,7 +689,11 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
                   }
                 }else{
                   Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
-                  //this can happen if evaluation is unknown
+                  //this can happen if evaluation is unknown, or if we are generalizing a star that already has a value
+                  if( !hasStar && d_quant_models[f].d_value[i]==d_false ){
+                    Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl;
+                  }
+                  Assert( hasStar || d_quant_models[f].d_value[i]!=d_false );
                   //might try it next effort level
                   d_star_insts[f].push_back(i);
                 }
@@ -780,11 +789,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       for( int i=0; i<riter.getNumTerms(); i++ ){
         Node rr = riter.getTerm( i );
         Node r = rr;
-        if( r.getType().isSort() ){
-          r = fm->getUsedRepresentative( r );
-        }else{
-          r = fm->getCurrentModelValue( r );
-        }
+        //if( r.getType().isSort() ){
+        r = fm->getUsedRepresentative( r );
+        //}else{
+        //  r = fm->getCurrentModelValue( r );
+        //}
         debugPrint("fmc-exh-debug", r);
         Trace("fmc-exh-debug") << " (term : " << rr << ")";
         ev_inst.push_back( r );
@@ -846,38 +855,12 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     d.addEntry(fm, mkCondDefault(fm, f), Node::null());
   }
   else if( n.getType().isArray() ){
-    //make the definition
-    bool success = false;
-    /*
-    Node r = fm->getRepresentative(n);
-    Trace("fmc-debug") << "Representative for array is " << r << std::endl;
-    while( r.getKind() == kind::STORE ){
-      Node i = fm->getUsedRepresentative( r[1] );
-      Node e = fm->getUsedRepresentative( r[2] );
-      d.addEntry(fm, mkArrayCond(i), e );
-      r = fm->getRepresentative( r[0] );
-    }
-    Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));
-    bool success = false;
-    Node odefaultValue;
-    if( r.getKind() == kind::STORE_ALL ){
-      ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();
-      odefaultValue = Node::fromExpr(storeAll.getExpr());
-      Node defaultValue = fm->getUsedRepresentative( odefaultValue, true );
-      if( !defaultValue.isNull() ){
-        d.addEntry(fm, defC, defaultValue);
-        success = true;
-      }
-    }
-    */
-    if( !success ){
-      //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
-      //Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
-      //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
-      //can't process this array
-      d.reset();
-      d.addEntry(fm, mkCondDefault(fm, f), Node::null());
-    }
+    //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
+    //Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
+    //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
+    //can't process this array
+    d.reset();
+    d.addEntry(fm, mkCondDefault(fm, f), Node::null());
   }
   else if( n.getNumChildren()==0 ){
     Node r = n;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 95b674cca..a698b33e1 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -50,8 +50,8 @@ bool QModelBuilder::optUseModel() {
 
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
-  if( Trace.isOn("quant-model-warn") ){
-    Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl;
+  if( Trace.isOn("quant-check-model") ){
+    Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
     int tests = 0;
     int bad = 0;
     for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -71,20 +71,20 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
           Node n = d_qe->getInstantiation( f, vars, terms );
           Node val = fm->getValue( n );
           if( val!=fm->d_true ){
-            Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
-            Trace("quant-model-warn") << "         " << f << std::endl;
-            Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
+            Trace("quant-check-model") << "*******  Instantiation " << n << " for " << std::endl;
+            Trace("quant-check-model") << "         " << f << std::endl;
+            Trace("quant-check-model") << "         Evaluates to " << val << std::endl;
             bad++;
           }
           riter.increment();
         }
-        Trace("quant-model-warn") << "Tested " << tests << " instantiations";
+        Trace("quant-check-model") << "Tested " << tests << " instantiations";
         if( bad>0 ){
-          Trace("quant-model-warn") << ", " << bad << " failed" << std::endl;
+          Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
         }
-        Trace("quant-model-warn") << "." << std::endl;
+        Trace("quant-check-model") << "." << std::endl;
       }else{
-        Trace("quant-model-warn") << "Warning: Could not test quantifier " << f << std::endl;
+        Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index a890276f7..5cff55d21 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -801,6 +801,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
   if( isVar ){
     Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
     if( n.getKind()==ITE ){
+  /*
       d_type = typ_ite_var;
       d_type_not = false;
       d_n = n;
@@ -817,8 +818,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
           }
         }
       }else{
+*/
         d_type = typ_invalid;
-      }
+     //}
     }else{
       d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
       d_qni_var_num[0] = qi->getVarNum( n );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 3c155c421..ff55c5c9b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1739,31 +1739,29 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     //check if it contains a quantifier as a subterm
     //if so, we will write this node
     if( containsQuantifiers( n ) ){
-      if( n.getType().isBoolean() ){
-        if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
-          if( options::preSkolemQuantAgg() ){
-            Node nn;
-            //must remove structure
-            if( n.getKind()==kind::ITE ){
-              nn = NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
-            }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
-              nn = NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
-            }else if( n.getKind()==kind::IMPLIES ){
-              nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
-            }
-            return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
-          }
-        }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
-          vector< Node > children;
-          for( int i=0; i<(int)n.getNumChildren(); i++ ){
-            children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
+      if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){
+        if( options::preSkolemQuantAgg() ){
+          Node nn;
+          //must remove structure
+          if( n.getKind()==kind::ITE ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+          }else if( n.getKind()==kind::IMPLIES ){
+            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
           }
-          return NodeManager::currentNM()->mkNode( n.getKind(), children );
+          return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
+        }
+      }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
+        vector< Node > children;
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
         }
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
       }
     }
   }
@@ -1771,15 +1769,20 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
 }
 
 Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+  Node prev = n;
   if( options::preSkolemQuant() ){
     if( !isInst || !options::preSkolemQuantNested() ){
-      //apply pre-skolemization to existential quantifiers
       Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+      //apply pre-skolemization to existential quantifiers
       std::vector< TypeNode > fvTypes;
       std::vector< TNode > fvs;
-      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs );
+      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
     }
   }
+  if( n!=prev ){       
+    Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl;
+    Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
+  }
   return n;
 }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3e5e30bd7..cb23b8bb7 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -59,16 +59,20 @@ TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) {
 }
 
 bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){
+  return addOrGetTerm( n, reps, argIndex )==n;
+}
+
+TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex ) {
   if( argIndex==(int)reps.size() ){
     if( d_data.empty() ){
       //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
       d_data[n].clear();
-      return true;
+      return n;
     }else{
-      return false;
+      return d_data.begin()->first;
     }
   }else{
-    return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 );
+    return d_data[reps[argIndex]].addOrGetTerm( n, reps, argIndex+1 );
   }
 }
 
@@ -502,9 +506,12 @@ void TermDb::reset( Theory::Effort effort ){
               Trace("term-db-debug") << d_arg_reps[n] << " ";
             }
             Trace("term-db-debug") << std::endl;
+            if( ee->hasTerm( n ) ){
+              Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+            }
           }
-
-          if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
+          Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
+          if( at!=n && ee->areEqual( at, n ) ){
             NoMatchAttribute nma;
             n.setAttribute(nma,true);
             Trace("term-db-debug") << n << " is redundant." << std::endl;
@@ -514,6 +521,7 @@ void TermDb::reset( Theory::Effort effort ){
             d_op_nonred_count[ it->first ]++;
           }
         }else{
+          Trace("term-db-debug") << n << " is already redundant." << std::endl;
           congruentCount++;
           alreadyCongruentCount++;
         }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index c770f0e6f..5560098c9 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -121,6 +121,7 @@ public:
   std::map< TNode, TermArgTrie > d_data;
 public:
   TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 );
+  TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
   bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
   void debugPrint( const char * c, Node n, unsigned depth = 0 );
   void clear() { d_data.clear(); }
diff --git a/test/regress/regress0/fmf/ForElimination-scala-9.smt2 b/test/regress/regress0/fmf/ForElimination-scala-9.smt2
new file mode 100644
index 000000000..36bb915f4
--- /dev/null
+++ b/test/regress/regress0/fmf/ForElimination-scala-9.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () ((Statement!1556 (Assign!1557 (varID!1558 (_ BitVec 32)) (expr!1559 Expression!1578)) (Block!1560 (body!1561 List!1617)) (For!1562 (init!1563 Statement!1556) (expr!1564 Expression!1578) (step!1565 Statement!1556) (body!1566 Statement!1556)) (IfThenElse!1567 (expr!1568 Expression!1578) (then!1569 Statement!1556) (elze!1570 Statement!1556)) (Print!1571 (msg!1572 (_ BitVec 32)) (varID!1573 (_ BitVec 32))) (Skip!1574) (While!1575 (expr!1576 Expression!1578) (body!1577 Statement!1556)))
+(Expression!1578 (And!1579 (lhs!1580 Expression!1578) (rhs!1581 Expression!1578)) (Division!1582 (lhs!1583 Expression!1578) (rhs!1584 Expression!1578)) (Equals!1585 (lhs!1586 Expression!1578) (rhs!1587 Expression!1578)) (GreaterThan!1588 (lhs!1589 Expression!1578) (rhs!1590 Expression!1578)) (IntLiteral!1591 (value!1592 (_ BitVec 32))) (LessThan!1593 (lhs!1594 Expression!1578) (rhs!1595 Expression!1578)) (Minus!1596 (lhs!1597 Expression!1578) (rhs!1598 Expression!1578)) (Modulo!1599 (lhs!1600 Expression!1578) (rhs!1601 Expression!1578)) (Neg!1602 (expr!1603 Expression!1578)) (Not!1604 (expr!1605 Expression!1578)) (Or!1606 (lhs!1607 Expression!1578) (rhs!1608 Expression!1578)) (Plus!1609 (lhs!1610 Expression!1578) (rhs!1611 Expression!1578)) (Times!1612 (lhs!1613 Expression!1578) (rhs!1614 Expression!1578)) (Var!1615 (varID!1616 (_ BitVec 32))))
+(List!1617 (Cons!1618 (head!1619 Statement!1556) (tail!1620 List!1617)) (Nil!1621))
+))
+(declare-fun error_value!1622 () Bool)
+(declare-fun ifree (Statement!1556) Bool)
+(declare-fun isForFreeList!223 (List!1617) Bool)
+(declare-fun error_value!1623 () List!1617)
+(declare-fun efll (List!1617) List!1617)
+(declare-fun efl (Statement!1556) Statement!1556)
+(declare-sort I_ifree 0)
+(set-info :notes "ifree_arg_0_1 is op created during fun def fmf")
+(declare-fun ifree_arg_0_1 (I_ifree) Statement!1556)
+(declare-sort I_isForFreeList!223 0)
+(set-info :notes "isForFreeList!223_arg_0_2 is op created during fun def fmf")
+(declare-fun isForFreeList!223_arg_0_2 (I_isForFreeList!223) List!1617)
+(declare-sort I_efll 0)
+(set-info :notes "efll_arg_0_3 is op created during fun def fmf")
+(declare-fun efll_arg_0_3 (I_efll) List!1617)
+(declare-sort I_efl 0)
+(set-info :notes "efl_arg_0_4 is op created during fun def fmf")
+(declare-fun efl_arg_0_4 (I_efl) Statement!1556)
+(assert (forall ((?i I_ifree)) (and (= (ifree (ifree_arg_0_1 ?i)) (ite (is-Block!1560 (ifree_arg_0_1 ?i)) (isForFreeList!223 (body!1561 (ifree_arg_0_1 ?i))) (ite (is-IfThenElse!1567 (ifree_arg_0_1 ?i)) (and (ifree (elze!1570 (ifree_arg_0_1 ?i))) (ifree (then!1569 (ifree_arg_0_1 ?i)))) (ite (is-While!1575 (ifree_arg_0_1 ?i)) (ifree (body!1577 (ifree_arg_0_1 ?i))) (not (is-For!1562 (ifree_arg_0_1 ?i))))))) (ite (is-Block!1560 (ifree_arg_0_1 ?i)) (not (forall ((?z I_isForFreeList!223)) (not (= (isForFreeList!223_arg_0_2 ?z) (body!1561 (ifree_arg_0_1 ?i)))) )) (ite (is-IfThenElse!1567 (ifree_arg_0_1 ?i)) (and (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (elze!1570 (ifree_arg_0_1 ?i)))) )) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (then!1569 (ifree_arg_0_1 ?i)))) ))) (ite (is-While!1575 (ifree_arg_0_1 ?i)) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (body!1577 (ifree_arg_0_1 ?i)))) )) true)))) ))
+(assert (forall ((?i I_isForFreeList!223)) (and (= (isForFreeList!223 (isForFreeList!223_arg_0_2 ?i)) (ite (is-Nil!1621 (isForFreeList!223_arg_0_2 ?i)) true (ite (is-Cons!1618 (isForFreeList!223_arg_0_2 ?i)) (and (isForFreeList!223 (tail!1620 (isForFreeList!223_arg_0_2 ?i))) (ifree (head!1619 (isForFreeList!223_arg_0_2 ?i)))) error_value!1622))) (ite (is-Nil!1621 (isForFreeList!223_arg_0_2 ?i)) true (ite (is-Cons!1618 (isForFreeList!223_arg_0_2 ?i)) (and (not (forall ((?z I_isForFreeList!223)) (not (= (isForFreeList!223_arg_0_2 ?z) (tail!1620 (isForFreeList!223_arg_0_2 ?i)))) )) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (head!1619 (isForFreeList!223_arg_0_2 ?i)))) ))) true))) ))
+(assert (forall ((?i I_efll)) (and (= (efll (efll_arg_0_3 ?i)) (ite (is-Nil!1621 (efll_arg_0_3 ?i)) Nil!1621 (ite (is-Cons!1618 (efll_arg_0_3 ?i)) (Cons!1618 (efl (head!1619 (efll_arg_0_3 ?i))) (efll (tail!1620 (efll_arg_0_3 ?i)))) error_value!1623))) (ite (is-Nil!1621 (efll_arg_0_3 ?i)) true (ite (is-Cons!1618 (efll_arg_0_3 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (head!1619 (efll_arg_0_3 ?i)))) )) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (tail!1620 (efll_arg_0_3 ?i)))) ))) true))) ))
+(assert (forall ((?i I_efl)) (and (= (efl (efl_arg_0_4 ?i)) (ite (is-Block!1560 (efl_arg_0_4 ?i)) (Block!1560 (efll (body!1561 (efl_arg_0_4 ?i)))) (ite (is-IfThenElse!1567 (efl_arg_0_4 ?i)) (IfThenElse!1567 (expr!1568 (efl_arg_0_4 ?i)) (efl (then!1569 (efl_arg_0_4 ?i))) (efl (elze!1570 (efl_arg_0_4 ?i)))) (ite (is-While!1575 (efl_arg_0_4 ?i)) (While!1575 (expr!1576 (efl_arg_0_4 ?i)) (efl (body!1577 (efl_arg_0_4 ?i)))) (ite (is-For!1562 (efl_arg_0_4 ?i)) (Block!1560 (Cons!1618 (efl (init!1563 (efl_arg_0_4 ?i))) (Cons!1618 (While!1575 (expr!1564 (efl_arg_0_4 ?i)) (Block!1560 (Cons!1618 (efl (body!1566 (efl_arg_0_4 ?i))) (Cons!1618 (efl (step!1565 (efl_arg_0_4 ?i))) Nil!1621)))) Nil!1621))) (efl_arg_0_4 ?i)))))) (ite (is-Block!1560 (efl_arg_0_4 ?i)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (efl_arg_0_4 ?i)))) )) (ite (is-IfThenElse!1567 (efl_arg_0_4 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (efl_arg_0_4 ?i)))) ))) (ite (is-While!1575 (efl_arg_0_4 ?i)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (efl_arg_0_4 ?i)))) )) (ite (is-For!1562 (efl_arg_0_4 ?i)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (efl_arg_0_4 ?i)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (efl_arg_0_4 ?i)))) ))) true))))) ))
+(assert (exists ((stat!216 Statement!1556)) (not (=> (and (and (and (and (is-For!1562 stat!216) (is-For!1562 stat!216)) (and (ifree (ite (is-Block!1560 (init!1563 stat!216)) (Block!1560 (efll (body!1561 (init!1563 stat!216)))) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (IfThenElse!1567 (expr!1568 (init!1563 stat!216)) (efl (then!1569 (init!1563 stat!216))) (efl (elze!1570 (init!1563 stat!216)))) (ite (is-While!1575 (init!1563 stat!216)) (While!1575 (expr!1576 (init!1563 stat!216)) (efl (body!1577 (init!1563 stat!216)))) (ite (is-For!1562 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (init!1563 stat!216))) (Cons!1618 (While!1575 (expr!1564 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (init!1563 stat!216))) (Cons!1618 (efl (step!1565 (init!1563 stat!216))) Nil!1621)))) Nil!1621))) (init!1563 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (init!1563 stat!216)) (Block!1560 (efll (body!1561 (init!1563 stat!216)))) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (IfThenElse!1567 (expr!1568 (init!1563 stat!216)) (efl (then!1569 (init!1563 stat!216))) (efl (elze!1570 (init!1563 stat!216)))) (ite (is-While!1575 (init!1563 stat!216)) (While!1575 (expr!1576 (init!1563 stat!216)) (efl (body!1577 (init!1563 stat!216)))) (ite (is-For!1562 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (init!1563 stat!216))) (Cons!1618 (While!1575 (expr!1564 (init!1563 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (init!1563 stat!216))) (Cons!1618 (efl (step!1565 (init!1563 stat!216))) Nil!1621)))) Nil!1621))) (init!1563 stat!216))))))) )) (ite (is-Block!1560 (init!1563 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (init!1563 stat!216)))) )) (ite (is-IfThenElse!1567 (init!1563 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (init!1563 stat!216)))) ))) (ite (is-While!1575 (init!1563 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (init!1563 stat!216)))) )) (ite (is-For!1562 (init!1563 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (init!1563 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (init!1563 stat!216)))) ))) true)))))) (and (ifree (ite (is-Block!1560 (step!1565 stat!216)) (Block!1560 (efll (body!1561 (step!1565 stat!216)))) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (IfThenElse!1567 (expr!1568 (step!1565 stat!216)) (efl (then!1569 (step!1565 stat!216))) (efl (elze!1570 (step!1565 stat!216)))) (ite (is-While!1575 (step!1565 stat!216)) (While!1575 (expr!1576 (step!1565 stat!216)) (efl (body!1577 (step!1565 stat!216)))) (ite (is-For!1562 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (step!1565 stat!216))) (Cons!1618 (While!1575 (expr!1564 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (step!1565 stat!216))) (Cons!1618 (efl (step!1565 (step!1565 stat!216))) Nil!1621)))) Nil!1621))) (step!1565 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (step!1565 stat!216)) (Block!1560 (efll (body!1561 (step!1565 stat!216)))) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (IfThenElse!1567 (expr!1568 (step!1565 stat!216)) (efl (then!1569 (step!1565 stat!216))) (efl (elze!1570 (step!1565 stat!216)))) (ite (is-While!1575 (step!1565 stat!216)) (While!1575 (expr!1576 (step!1565 stat!216)) (efl (body!1577 (step!1565 stat!216)))) (ite (is-For!1562 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (step!1565 stat!216))) (Cons!1618 (While!1575 (expr!1564 (step!1565 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (step!1565 stat!216))) (Cons!1618 (efl (step!1565 (step!1565 stat!216))) Nil!1621)))) Nil!1621))) (step!1565 stat!216))))))) )) (ite (is-Block!1560 (step!1565 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (step!1565 stat!216)))) )) (ite (is-IfThenElse!1567 (step!1565 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (step!1565 stat!216)))) ))) (ite (is-While!1575 (step!1565 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (step!1565 stat!216)))) )) (ite (is-For!1562 (step!1565 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (step!1565 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (step!1565 stat!216)))) ))) true)))))) (and (ifree (ite (is-Block!1560 (body!1566 stat!216)) (Block!1560 (efll (body!1561 (body!1566 stat!216)))) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (IfThenElse!1567 (expr!1568 (body!1566 stat!216)) (efl (then!1569 (body!1566 stat!216))) (efl (elze!1570 (body!1566 stat!216)))) (ite (is-While!1575 (body!1566 stat!216)) (While!1575 (expr!1576 (body!1566 stat!216)) (efl (body!1577 (body!1566 stat!216)))) (ite (is-For!1562 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (body!1566 stat!216))) (Cons!1618 (While!1575 (expr!1564 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (body!1566 stat!216))) (Cons!1618 (efl (step!1565 (body!1566 stat!216))) Nil!1621)))) Nil!1621))) (body!1566 stat!216)))))) (not (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 (body!1566 stat!216)) (Block!1560 (efll (body!1561 (body!1566 stat!216)))) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (IfThenElse!1567 (expr!1568 (body!1566 stat!216)) (efl (then!1569 (body!1566 stat!216))) (efl (elze!1570 (body!1566 stat!216)))) (ite (is-While!1575 (body!1566 stat!216)) (While!1575 (expr!1576 (body!1566 stat!216)) (efl (body!1577 (body!1566 stat!216)))) (ite (is-For!1562 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (init!1563 (body!1566 stat!216))) (Cons!1618 (While!1575 (expr!1564 (body!1566 stat!216)) (Block!1560 (Cons!1618 (efl (body!1566 (body!1566 stat!216))) (Cons!1618 (efl (step!1565 (body!1566 stat!216))) Nil!1621)))) Nil!1621))) (body!1566 stat!216))))))) )) (ite (is-Block!1560 (body!1566 stat!216)) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 (body!1566 stat!216)))) )) (ite (is-IfThenElse!1567 (body!1566 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 (body!1566 stat!216)))) ))) (ite (is-While!1575 (body!1566 stat!216)) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 (body!1566 stat!216)))) )) (ite (is-For!1562 (body!1566 stat!216)) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 (body!1566 stat!216)))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 (body!1566 stat!216)))) ))) true)))))) (or (ifree (ite (is-Block!1560 stat!216) (Block!1560 (efll (body!1561 stat!216))) (ite (is-IfThenElse!1567 stat!216) (IfThenElse!1567 (expr!1568 stat!216) (efl (then!1569 stat!216)) (efl (elze!1570 stat!216))) (ite (is-While!1575 stat!216) (While!1575 (expr!1576 stat!216) (efl (body!1577 stat!216))) (ite (is-For!1562 stat!216) (Block!1560 (Cons!1618 (efl (init!1563 stat!216)) (Cons!1618 (While!1575 (expr!1564 stat!216) (Block!1560 (Cons!1618 (efl (body!1566 stat!216)) (Cons!1618 (efl (step!1565 stat!216)) Nil!1621)))) Nil!1621))) stat!216))))) (forall ((?z I_ifree)) (not (= (ifree_arg_0_1 ?z) (ite (is-Block!1560 stat!216) (Block!1560 (efll (body!1561 stat!216))) (ite (is-IfThenElse!1567 stat!216) (IfThenElse!1567 (expr!1568 stat!216) (efl (then!1569 stat!216)) (efl (elze!1570 stat!216))) (ite (is-While!1575 stat!216) (While!1575 (expr!1576 stat!216) (efl (body!1577 stat!216))) (ite (is-For!1562 stat!216) (Block!1560 (Cons!1618 (efl (init!1563 stat!216)) (Cons!1618 (While!1575 (expr!1564 stat!216) (Block!1560 (Cons!1618 (efl (body!1566 stat!216)) (Cons!1618 (efl (step!1565 stat!216)) Nil!1621)))) Nil!1621))) stat!216)))))) ) (not (ite (is-Block!1560 stat!216) (not (forall ((?z I_efll)) (not (= (efll_arg_0_3 ?z) (body!1561 stat!216))) )) (ite (is-IfThenElse!1567 stat!216) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (then!1569 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (elze!1570 stat!216))) ))) (ite (is-While!1575 stat!216) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1577 stat!216))) )) (ite (is-For!1562 stat!216) (and (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (init!1563 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (body!1566 stat!216))) )) (not (forall ((?z I_efl)) (not (= (efl_arg_0_4 ?z) (step!1565 stat!216))) ))) true)))))))) ))
+(check-sat)
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index aa3508798..2e075176c 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -52,8 +52,8 @@ TESTS =	\
 	am-bad-model.cvc \
 	nun-0208-to.smt2 \
 	datatypes-ufinite.smt2 \
-	datatypes-ufinite-nested.smt2
-
+	datatypes-ufinite-nested.smt2 \
+	ForElimination-scala-9.smt2
 
 EXTRA_DIST = $(TESTS)