summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r--src/theory/quantifiers_engine.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index afc607470..2177ebc32 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -767,7 +767,7 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool
bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
// For resource-limiting (also does a time check).
- getOutputChannel().safePoint();
+ getOutputChannel().safePoint(options::quantifierStep());
Assert( terms.size()==f[0].getNumChildren() );
Trace("inst-add-debug") << "Add instantiation: ";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback