diff options
Diffstat (limited to 'src/theory/quantifiers/modes.h')
| -rw-r--r-- | src/theory/quantifiers/modes.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index acc883f2a..80dbb783e 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -62,14 +62,10 @@ typedef enum { MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, - /** implementation that mimics inst-gen */ - MBQI_INST_GEN, /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ MBQI_FMC_INTERVAL, - /** mbqi with interval abstraction of uninterpreted sorts */ - MBQI_INTERVAL, /** abstract mbqi algorithm */ MBQI_ABS, /** mbqi trust (produce no instantiations) */ |