summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_modes.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-07-02 20:08:53 -0500
committerGitHub <noreply@github.com>2018-07-02 20:08:53 -0500
commit0dec323ac1b45ce1ca194e9bb2a335c8def525d2 (patch)
treec201933c725ddfd7f68a1e03db8e4f85242d0d6c /src/options/quantifiers_modes.h
parentbe58c8ead1d36ab3625faf848b2ebdce8d5de8a9 (diff)
Remove miscellaneous dead and unused code from quantifiers (#2121)
Diffstat (limited to 'src/options/quantifiers_modes.h')
-rw-r--r--src/options/quantifiers_modes.h2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 33c047d23..a949b97be 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -59,8 +59,6 @@ enum MbqiMode {
MBQI_NONE,
/** default, mbqi from Section 5.4.2 of AJR thesis */
MBQI_FMC,
- /** mbqi with integer intervals */
- MBQI_FMC_INTERVAL,
/** abstract mbqi algorithm */
MBQI_ABS,
/** mbqi trust (produce no instantiations) */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback