summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_strategy_cbqi.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 668593842..bd2b8e78e 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -744,7 +744,6 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
}else{
//this should never happen for monotonic selection strategies
Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
- Assert( !options::cbqiNestedQE() || options::cbqiAll() );
return false;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback