diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 1 |
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() ){ |