3 files changed, 6 insertions, 22 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 420396452..36144e70e 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -267,7 +267,8 @@ agg \n\
 \n\
 ";
 
-const std::string OptionsHandler::s_mbqiModeHelp = "\
+const std::string OptionsHandler::s_mbqiModeHelp =
+    "\
 Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
 \n\
 default \n\
@@ -277,12 +278,8 @@ default \n\
 none \n\
 + Disable model-based quantifier instantiation.\n\
 \n\
-gen-ev \n\
-+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper based on generalizing evaluations.\n\
-\n\
-abs \n\
-+ Use abstract MBQI algorithm (uses disjoint sets). \n\
+trust \n\
++ Do not instantiate quantified formulas (incomplete technique).\n\
 \n\
 ";
 
@@ -660,14 +657,11 @@ void OptionsHandler::checkLiteralMatchMode(
 theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(
     std::string option, std::string optarg)
 {
-  if(optarg == "gen-ev") {
-    return theory::quantifiers::MBQI_GEN_EVAL;
-  } else if(optarg == "none") {
+  if (optarg == "none")
+  {
     return theory::quantifiers::MBQI_NONE;
   } else if(optarg == "default" || optarg ==  "fmc") {
     return theory::quantifiers::MBQI_FMC;
-  } else if(optarg == "abs") {
-    return theory::quantifiers::MBQI_ABS;
   } else if(optarg == "trust") {
     return theory::quantifiers::MBQI_TRUST;
   } else if(optarg == "help") {
diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp
index 1814a363d..b08f71c2e 100644
--- a/src/options/quantifiers_modes.cpp
+++ b/src/options/quantifiers_modes.cpp
@@ -64,18 +64,12 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod
 
 std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
   switch(mode) {
-  case theory::quantifiers::MBQI_GEN_EVAL:
-    out << "MBQI_GEN_EVAL";
-    break;
   case theory::quantifiers::MBQI_NONE:
     out << "MBQI_NONE";
     break;
   case theory::quantifiers::MBQI_FMC:
     out << "MBQI_FMC";
     break;
-  case theory::quantifiers::MBQI_ABS:
-    out << "MBQI_ABS";
-    break;
   case theory::quantifiers::MBQI_TRUST:
     out << "MBQI_TRUST";
     break;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 41378d2cd..eea043865 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -53,14 +53,10 @@ enum LiteralMatchMode {
 };
 
 enum MbqiMode {
-  /** mbqi from CADE 24 paper */
-  MBQI_GEN_EVAL,
   /** no mbqi */
   MBQI_NONE,
   /** default, mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
-  /** abstract mbqi algorithm */
-  MBQI_ABS,
   /** mbqi trust (produce no instantiations) */
   MBQI_TRUST,
 };