summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 11ff9ecad..c1476acb8 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -183,6 +183,8 @@ void InstantiationEngine::check( Theory::Effort e ){
// such that the counterexample literal is not in positive in d_counterexample_asserts
// for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
// if( (*i).second ) {
+ Debug("quantifiers") << "quantifiers: check: asserted quantifiers size"
+ << getQuantifiersEngine()->getNumAssertedQuantifiers() << std::endl;
for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
Node n = getQuantifiersEngine()->getAssertedQuantifier( i );
if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback