summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bounded_integers.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.h')
-rw-r--r--src/theory/quantifiers/bounded_integers.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index ac188ca65..355360e41 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -110,7 +110,8 @@ private:
public:
BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
- void check( Theory::Effort e );
+ bool needsCheck( Theory::Effort e );
+ void check( Theory::Effort e, unsigned quant_e );
void registerQuantifier( Node f );
void assertNode( Node n );
Node getNextDecisionRequest();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback