Cleanup quantifier elimination in smt engine.

2 files changed, 2 insertions, 1 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index f3061f575..71c0858bf 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -370,7 +370,7 @@ Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< No
   // there is a nested quantified formula (forall y. nq[y,x]) such that 
   //    q is (forall y. nq[y,t]) for ground terms t,
   //    ceq is (forall y. nq[y,e]) for CE variables e.
-  // we call this function when we know (exists e. ceq[e,k]) is equivalent to quantifier-free formula C[k].
+  // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
   // in this case, q is equivalent to the quantifier-free formula C[t].
   if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
     d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 57eb375d3..c412b2c3a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1464,6 +1464,7 @@ void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  )
 }
 
 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
+  Assert( q.getKind()==FORALL );
   std::vector< Node > insts;
   getInstantiations( q, insts );
   if( insts.empty() ){