Minor change to F-Length inference in strings. No internal tracking of cardinality...

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8f1ba5fca1bbd28e48ec685797362309221c4c4c..63178543756ab51ce5c71194b826b7e492175eed 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1133,7 +1133,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
   TypeSet defaultValuesSet;
 
   // Compute all default values already in use
-  if (fullModel) {
+  //if (fullModel) {
     for (size_t i=0; i<arrays.size(); ++i) {
       TNode nrep = d_equalityEngine.getRepresentative(arrays[i]);
       d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
@@ -1143,14 +1143,14 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
         defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second);
       }
     }
-  }
+  //}
 
   // Loop through all array equivalence classes that need a representative computed
   for (size_t i=0; i<arrays.size(); ++i) {
     TNode n = arrays[i];
     TNode nrep = d_equalityEngine.getRepresentative(n);
 
-    if (fullModel) {
+    //if (fullModel) {
       // Compute default value for this array - there is one default value for every mayEqual equivalence class
       TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
       it = d_defValues.find(mayRep);
@@ -1171,6 +1171,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
 
       // Build the STORE_ALL term with the default value
       rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr()));
+      /*
     }
     else {
       std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
@@ -1182,6 +1183,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
         rep = (*it).second;
       }
     }
+*/
 
     // For each read, require that the rep stores the right value
     vector<Node>& reads = selects[nrep];

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index e44a322b5e95aea46d584744cc89fe406541ba19..98cd175fd3dc6ea1ee09d821098e53ca673388df 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -461,7 +461,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
             }
           }
           if( !isStar && !ri.isConst() ){
-            Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
+            Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
             Assert( false );
           }
           entry_children.push_back(ri);
@@ -469,7 +469,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
         Node nv = fm->getUsedRepresentative( v );
         if( !nv.isConst() ){
-          Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;
+          Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
           Assert( false );
         }
         Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
@@ -690,10 +690,12 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
                 }else{
                   Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
                   //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 );
+                  //if( !hasStar && d_quant_models[f].d_value[i]==d_false ){
+                  //  Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl;
+                  //}
+                  //this assertion can happen if two instantiations from this round are identical
+                  // (0,1)->false (1,0)->false   for   forall xy. f( x, y ) = f( y, x )
+                  //Assert( hasStar || d_quant_models[f].d_value[i]!=d_false );
                   //might try it next effort level
                   d_star_insts[f].push_back(i);
                 }

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9f474a3ca9935772786a3b041b4a6b8097476787..634c1b1304c03fd6b984d5956a79ee6248429f86 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1417,8 +1417,9 @@ void TheoryStrings::checkFlatForms() {
               }else{
                 Node curr = d_flat_form[a][count];
                 Node curr_c = d_eqc_to_const[curr];
+                Node ac = a[d_flat_form_index[a][count]];
                 std::vector< Node > lexp;
-                Node lcurr = getLength( curr, lexp );
+                Node lcurr = getLength( ac, lexp );
                 for( unsigned i=1; i<it->second.size(); i++ ){
                   b = it->second[i];
                   if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
@@ -1438,7 +1439,6 @@ void TheoryStrings::checkFlatForms() {
                     }else{
                       Node cc = d_flat_form[b][count];
                       if( cc!=curr ){
-                        Node ac = a[d_flat_form_index[a][count]];
                         Node bc = b[d_flat_form_index[b][count]];
                         inelig.push_back( b );
                         Assert( !areEqual( curr, cc ) );
@@ -1463,10 +1463,14 @@ void TheoryStrings::checkFlatForms() {
                         }else{
                           //if lengths are the same, apply LengthEq
                           std::vector< Node > lexp2;
-                          Node lcc = getLength( cc, lexp2 );
+                          Node lcc = getLength( bc, lexp2 );
                           if( areEqual( lcurr, lcc ) ){
                             Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl;
                             //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
+                            Trace("strings-ff-debug") << "Explanation for " << lcurr << " is ";
+                            for( unsigned j=0; j<lexp.size(); j++ ) { Trace("strings-ff-debug") << lexp[j] << std::endl; }
+                            Trace("strings-ff-debug") << "Explanation for " << lcc << " is ";
+                            for( unsigned j=0; j<lexp2.size(); j++ ) { Trace("strings-ff-debug") << lexp2[j] << std::endl; }
                             exp.insert( exp.end(), lexp.begin(), lexp.end() );
                             exp.insert( exp.end(), lexp2.begin(), lexp2.end() );
                             addToExplanation( lcurr, lcc, exp );
@@ -2755,6 +2759,7 @@ void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >
       for( unsigned i=0; i<exp_n.size(); i++ ){
         Trace("strings-infer-debug")  << "  N:" << exp_n[i] << std::endl;
       }
+      //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
     }
     bool doSendLemma = ( asLemma || eq==d_false || eq.getKind()==kind::OR || options::stringInferAsLemmas() );
     if( doSendLemma ){  

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 977b9f4c1e9576a4dccd4a2edd2335d3593a7a6e..1f18416c5aa1c23606d5809787fc0b0051a3bf1f 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -407,7 +407,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
 StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
           d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
           d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
-          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){
+          d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){
   d_cardinality_term = n;
   //if( d_type.isSort() ){
   //  TypeEnumerator te(tn);
@@ -723,11 +723,13 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){
     if( !d_hasCard || i<d_cardinality ){
       Node cn = d_cardinality_literal[ i ];
       Assert( !cn.isNull() );
-      if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
+      bool value;
+      if( !d_thss->getTheory()->d_valuation.hasSatValue( cn, value ) ){
         Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl;
         return cn;
       }else{
-        Trace("uf-ss-dec-debug") << "  dec : " << cn << " already asserted " << d_cardinality_assertions[cn].get() << std::endl;
+        Trace("uf-ss-dec-debug") << "  dec : " << cn << " already asserted " << value << std::endl;
+        Assert( !value );
       }
     }
   }
@@ -846,7 +848,6 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
     Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
     Assert( c>0 );
     Node cl = getCardinalityLiteral( c );
-    d_cardinality_assertions[ cl ] = val;
     if( val ){
       bool doCheckRegions = !d_hasCard;
       bool prevHasCard = d_hasCard;
@@ -890,8 +891,9 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
         bool needsCard = true;
         for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){
           if( it->first<=d_aloc_cardinality.get() ){
-            if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
-              Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl;
+            bool value;
+            if( !d_thss->getTheory()->d_valuation.hasSatValue( it->second, value ) ){
+              Debug("fmf-card-debug") << "..does not need allocate because we are waiting for " << it->second << std::endl;
               needsCard = false;
               break;
             }
@@ -1028,14 +1030,21 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 
   //allocate the lowest such that it is not asserted
   Node cl;
+  bool increment;
   do {
+    increment = false;
     d_aloc_cardinality = d_aloc_cardinality + 1;
     cl = getCardinalityLiteral( d_aloc_cardinality );
-  }while( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() && !d_cardinality_assertions[cl] );
-  //if one is already asserted postively, abort
-  if( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() ){
-    return;
-  }
+    bool value;
+    if( d_thss->getTheory()->d_valuation.hasSatValue( cl, value ) ){
+      if( value ){
+        //if one is already asserted postively, abort
+        return;
+      }else{
+        increment = true;
+      }
+    }
+  }while( increment );
 
   //check for abort case
   if( options::ufssAbortCardinality()==d_aloc_cardinality ){

diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index db4c50423c938d9bd1ba2ee458752e3740f209ae..3dfaed663f0201d45bd5f1a137dc3b0768b5d82c 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -232,8 +232,6 @@ public:
     std::map< int, Node > d_cardinality_literal;
     /** cardinality lemmas */
     std::map< int, Node > d_cardinality_lemma;
-    /** cardinality assertions (indexed by cardinality literals ) */
-    NodeBoolMap d_cardinality_assertions;
     /** whether a positive cardinality constraint has been asserted */
     context::CDO< bool > d_hasCard;
     /** clique lemmas that have been asserted */

diff --git a/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2
new file mode 100644 (file)
index 0000000..9ef5f14
--- /dev/null
+++ b/test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2
@@ -0,0 +1,33 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((array!896 (array!896!897 (size!898 (_ BitVec 32)) (content!899 (Array (_ BitVec 32) (_ BitVec 32)))))))
+(declare-datatypes () ((tuple2!900 (tuple2!900!901 (_1!902 array!896) (_2!903 (_ BitVec 32))))))
+(declare-fun error_value!904 () (_ BitVec 32))
+(declare-fun error_value!905 () (_ BitVec 32))
+(declare-fun error_value!906 () array!896)
+(declare-fun error_value!907 () (_ BitVec 32))
+(declare-fun error_value!908 () array!896)
+(declare-fun error_value!909 () (_ BitVec 32))
+(declare-fun while0!216 (array!896 (_ BitVec 32) array!896) tuple2!900)
+(declare-fun isPositive!206 (array!896 (_ BitVec 32)) Bool)
+(declare-fun rec!210 ((_ BitVec 32) array!896 (_ BitVec 32)) Bool)
+(declare-fun arrayconst!910 () (Array (_ BitVec 32) (_ BitVec 32)))
+(declare-sort I_while0!216 0)
+(declare-fun while0!216_arg_0_1 (I_while0!216) array!896)
+(declare-fun while0!216_arg_1_2 (I_while0!216) (_ BitVec 32))
+(declare-fun while0!216_arg_2_3 (I_while0!216) array!896)
+(declare-sort I_isPositive!206 0)
+(declare-fun isPositive!206_arg_0_4 (I_isPositive!206) array!896)
+(declare-fun isPositive!206_arg_1_5 (I_isPositive!206) (_ BitVec 32))
+(declare-sort I_rec!210 0)
+(declare-fun rec!210_arg_0_6 (I_rec!210) (_ BitVec 32))
+(declare-fun rec!210_arg_1_7 (I_rec!210) array!896)
+(declare-fun rec!210_arg_2_8 (I_rec!210) (_ BitVec 32))
+(assert (forall ((?i I_while0!216)) (and (= (while0!216 (while0!216_arg_0_1 ?i) (while0!216_arg_1_2 ?i) (while0!216_arg_2_3 ?i)) (ite (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (while0!216 (ite (bvslt (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!904) (_ bv0 32)) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (bvneg (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!905)))) error_value!906) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!907))) error_value!908)) (bvadd (while0!216_arg_1_2 ?i) (_ bv1 32)) (while0!216_arg_2_3 ?i)) (tuple2!900!901 (while0!216_arg_0_1 ?i) (while0!216_arg_1_2 ?i)))) (ite (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (ite (bvslt (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!904) (_ bv0 32)) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (bvneg (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!905)))) error_value!906) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_0_1 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (array!896!897 (size!898 (while0!216_arg_0_1 ?i)) (store (content!899 (while0!216_arg_0_1 ?i)) (while0!216_arg_1_2 ?i) (ite (and (bvslt (while0!216_arg_1_2 ?i) (size!898 (while0!216_arg_2_3 ?i))) (not (bvslt (while0!216_arg_1_2 ?i) (_ bv0 32)))) (select (content!899 (while0!216_arg_2_3 ?i)) (while0!216_arg_1_2 ?i)) error_value!907))) error_value!908))) (= (while0!216_arg_1_2 ?z) (bvadd (while0!216_arg_1_2 ?i) (_ bv1 32))) (= (while0!216_arg_2_3 ?z) (while0!216_arg_2_3 ?i)))) )) true)) ))
+(assert (forall ((?i I_isPositive!206)) (and (= (isPositive!206 (isPositive!206_arg_0_4 ?i) (isPositive!206_arg_1_5 ?i)) (rec!210 (_ bv0 32) (isPositive!206_arg_0_4 ?i) (isPositive!206_arg_1_5 ?i))) (not (forall ((?z I_rec!210)) (not (and (= (rec!210_arg_0_6 ?z) (_ bv0 32)) (= (rec!210_arg_1_7 ?z) (isPositive!206_arg_0_4 ?i)) (= (rec!210_arg_2_8 ?z) (isPositive!206_arg_1_5 ?i)))) ))) ))
+(assert (forall ((?i I_rec!210)) (and (= (rec!210 (rec!210_arg_0_6 ?i) (rec!210_arg_1_7 ?i) (rec!210_arg_2_8 ?i)) (ite (not (bvslt (rec!210_arg_0_6 ?i) (rec!210_arg_2_8 ?i))) true (ite (bvslt (ite (and (bvslt (rec!210_arg_0_6 ?i) (size!898 (rec!210_arg_1_7 ?i))) (not (bvslt (rec!210_arg_0_6 ?i) (_ bv0 32)))) (select (content!899 (rec!210_arg_1_7 ?i)) (rec!210_arg_0_6 ?i)) error_value!909) (_ bv0 32)) false (rec!210 (bvadd (rec!210_arg_0_6 ?i) (_ bv1 32)) (rec!210_arg_1_7 ?i) (rec!210_arg_2_8 ?i))))) (ite (not (bvslt (rec!210_arg_0_6 ?i) (rec!210_arg_2_8 ?i))) true (ite (bvslt (ite (and (bvslt (rec!210_arg_0_6 ?i) (size!898 (rec!210_arg_1_7 ?i))) (not (bvslt (rec!210_arg_0_6 ?i) (_ bv0 32)))) (select (content!899 (rec!210_arg_1_7 ?i)) (rec!210_arg_0_6 ?i)) error_value!909) (_ bv0 32)) true (not (forall ((?z I_rec!210)) (not (and (= (rec!210_arg_0_6 ?z) (bvadd (rec!210_arg_0_6 ?i) (_ bv1 32))) (= (rec!210_arg_1_7 ?z) (rec!210_arg_1_7 ?i)) (= (rec!210_arg_2_8 ?z) (rec!210_arg_2_8 ?i)))) ))))) ))
+(assert (not (forall ((tab!211 array!896)) (or (or (bvslt (size!898 (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211))) (_ bv0 32)) (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (array!896!897 (size!898 tab!211) arrayconst!910)) (= (while0!216_arg_1_2 ?z) (_ bv0 32)) (= (while0!216_arg_2_3 ?z) tab!211))) )) (or (isPositive!206 (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211)) (size!898 tab!211)) (forall ((?z I_isPositive!206)) (not (and (= (isPositive!206_arg_0_4 ?z) (_1!902 (while0!216 (array!896!897 (size!898 tab!211) arrayconst!910) (_ bv0 32) tab!211))) (= (isPositive!206_arg_1_5 ?z) (size!898 tab!211)))) ) (forall ((?z I_while0!216)) (not (and (= (while0!216_arg_0_1 ?z) (array!896!897 (size!898 tab!211) arrayconst!910)) (= (while0!216_arg_1_2 ?z) (_ bv0 32)) (= (while0!216_arg_2_3 ?z) tab!211))) ))) )))
+(check-sat)
+

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 2e075176c96cbe429b2e133c9a62ddd366e9903c..575aa4159d6b9883b5e63b962edc8cc74cac276b 100644 (file)
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -53,7 +53,9 @@ TESTS =       \
        nun-0208-to.smt2 \
        datatypes-ufinite.smt2 \
        datatypes-ufinite-nested.smt2 \
-       ForElimination-scala-9.smt2
+       ForElimination-scala-9.smt2 \
+       agree466.smt2 \
+       LeftistHeap.scala-8-ncm.smt2
 
 EXTRA_DIST = $(TESTS)
 
@@ -68,7 +70,6 @@ EXTRA_DIST = $(TESTS)
 #EXTRA_DIST += \
 #      error.cvc
 
-# agree466.smt2 timeout after commit on 1/14 due to Array+FMF model construction
 
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test