summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/fmf/bounded_integers.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.cpp')
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index ef6926bcb..cafa4a749 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -275,7 +275,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
bool BoundedIntegers::needsCheck(Theory::Effort e)
{
- return e == Theory::EFFORT_FULL;
+ return e == Theory::EFFORT_LAST_CALL;
}
void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback