Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3670e8cb9..82d3139b2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5138,6 +5138,8 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
       ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
       InternalError(ss.str().c_str());
     }
+    
+ #if 1
     //get the instantiations for all quantified formulas
     std::map< Node, std::vector< Node > > insts;
     d_theoryEngine->getInstantiations( insts );
@@ -5168,7 +5170,10 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
         ss << " that was not related to the query.  Try option --simplification=none.";
         InternalError(ss.str().c_str());
       }
-    }
+    }   
+#else
+    Node ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
+#endif
     Trace("smt-qe") << "Returned : " << ret_n << std::endl;
     ret_n = Rewriter::rewrite( ret_n.negate() );
     return ret_n.toExpr();