diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2bebabc5a..d81efe1da 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1041,16 +1041,20 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo #ifdef CVC4_ASSERTIONS bool bad_inst = false; if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){ + Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl; bad_inst = true; }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){ + Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl; bad_inst = true; }else if( options::cbqi() ){ Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]); if( !icf.isNull() ){ if( icf==q ){ + Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl; + bad_inst = true; + }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){ + Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl; bad_inst = true; - }else{ - bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ); } } } |