summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/modes.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/modes.h')
-rw-r--r--src/theory/quantifiers/modes.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index b37e48ec3..89e10b175 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -70,6 +70,8 @@ typedef enum {
MBQI_FMC_INTERVAL,
/** mbqi with interval abstraction of uninterpreted sorts */
MBQI_INTERVAL,
+ /** mbqi trust (produce no instantiations) */
+ MBQI_TRUST,
} MbqiMode;
typedef enum {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback