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

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ff0da13e1a23209993c7424516ac8fc36eb869c1..e44a322b5e95aea46d584744cc89fe406541ba19 100644 (file)
--- 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 95b674ccad5f981dbeecf115a5a10ab5dfa2a92f..a698b33e1aa70dd5692a7485ff7f0d402958d8e3 100644 (file)
--- 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 a890276f7905da6fdbaf0f8a115dbbab2fd22733..5cff55d212316925ec0c1423522f6c132d79275b 100644 (file)
--- 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 3c155c421b1eaca4a23922312dbafb1cced0b353..ff55c5c9b23dcdf563a5e3b0d32e529da9a72a16 100644 (file)
--- 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 3e5e30bd708a44bf53dd9506bf78de1013f19003..cb23b8bb7afce1df39d75a9c395dc7abec81eff0 100644 (file)
--- 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 c770f0e6f9d8fb1747bd7f075aea84fedd933f27..5560098c9ab7ebc59205f85f07f3f817efef5543 100644 (file)
--- 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 (file)
index 0000000..36bb915
--- /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 aa350879833c4eb1ba1c7861a31cf83d62c99a79..2e075176c96cbe429b2e133c9a62ddd366e9903c 100644 (file)
--- 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)