summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_instantiation.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-07-20 19:46:21 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2015-07-20 19:46:21 +0200
commitf62d9456b41bf17df1d339e46776c9213cb3705a (patch)
tree01d3448b3c9fe89ead56c72b18f8516292092e13 /src/theory/quantifiers/ce_guided_instantiation.h
parent7943953741c67d8246f983e193d26812d959b4cd (diff)
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.h')
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 74e9b0aba..5f393626c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -83,6 +83,8 @@ public: //for fairness
CegqiFairMode getCegqiFairMode();
/** is single invocation */
bool isSingleInvocation();
+ /** needs check */
+ bool needsCheck();
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback