4 files changed, 60 insertions, 4 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a3617ef6f..351c8b608 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -446,6 +446,23 @@ all \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_cbqiBvIneqModeHelp =
+    "\
+Modes for single invocation techniques, supported by --cbqi-bv-ineq:\n\
+\n\
+eq-slack (default)  \n\
++ Solve for the inequality using the slack value in the model, e.g.,\
+  t > s becomes t = s + ( t-s )^M.\n\
+\n\
+eq-boundary \n\
++ Solve for the boundary point of the inequality, e.g.,\
+  t > s becomes t = s+1.\n\
+\n\
+keep  \n\
++ Solve for the inequality directly using side conditions for invertibility.\n\
+\n\
+";
+
 const std::string OptionsHandler::s_cegqiSingleInvHelp = "\
 Modes for single invocation techniques, supported by --cegqi-si:\n\
 \n\
@@ -772,6 +789,34 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s
   }
 }
 
+theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode(
+    std::string option, std::string optarg) throw(OptionException)
+{
+  if (optarg == "eq-slack")
+  {
+    return theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK;
+  }
+  else if (optarg == "eq-boundary")
+  {
+    return theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY;
+  }
+  else if (optarg == "keep")
+  {
+    return theory::quantifiers::CBQI_BV_INEQ_KEEP;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_cbqiBvIneqModeHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --cbqi-bv-ineq: `")
+                          + optarg
+                          + "'.  Try --cbqi-bv-ineq help.");
+  }
+}
+
 theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "none" ) {
     return theory::quantifiers::CEGQI_SI_MODE_NONE;
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index e534d8e58..c525c9e0e 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -98,6 +98,8 @@ public:
   theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::CbqiBvIneqMode stringToCbqiBvIneqMode(
+      std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
@@ -216,6 +218,7 @@ public:
   static const std::string s_qcfModeHelp;
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
+  static const std::string s_cbqiBvIneqModeHelp;
   static const std::string s_cegqiSingleInvHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_termDbModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 0b410e3fe..a19555987 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -149,6 +149,16 @@ enum IteLiftQuantMode {
   ITE_LIFT_QUANT_MODE_ALL,
 };
 
+enum CbqiBvIneqMode
+{
+  /** solve for inequalities using slack values in model */
+  CBQI_BV_INEQ_EQ_SLACK,
+  /** solve for inequalities using boundary points */
+  CBQI_BV_INEQ_EQ_BOUNDARY,
+  /** solve for inequalities directly, using side conditions */
+  CBQI_BV_INEQ_KEEP,
+};
+
 enum CegqiSingleInvMode {
   /** do not use single invocation techniques */
   CEGQI_SI_MODE_NONE,
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 05c2512cd..0262012f6 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -337,10 +337,8 @@ option cbqiBv --cbqi-bv bool :read-write :default false
   use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors
 option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false
   interleave model value instantiation with word-level inversion approach
-option cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true
-  use model slack values when solving inequalities with word-level inversion approach
-option cbqiBvInvInDisEq --cbqi-bv-inv-in-dis-eq bool :read-write :default false
-  let bv inverter handle (un)signed less than nodes
+option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode
+ choose mode for handling bit-vector inequalities with counterexample-guided instantiation
  
 ### local theory extensions options