summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_conflict_find.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c796333b3..ca87a607d 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2004,7 +2004,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
Assert( !getTermDatabase()->isEntailed( inst, true ) );
Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
}
- if( d_quantEngine->addInstantiation( q, terms, false ) ){
+ if( d_quantEngine->addInstantiation( q, terms ) ){
Trace("qcf-check") << " ... Added instantiation" << std::endl;
Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
qi->debugPrintMatch("qcf-inst");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback