CegqiBv: Clean up after renaming options. (#4487)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 21cba6abb9e5d856d6ed57741f58f39d16040ce3..1834c90c496ee360120ed7f50bacd4c746b1913e 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1763,7 +1763,7 @@ header = "options/quantifiers_options.h"
   long       = "quant-epr"
   type       = "bool"
   default    = "false"
-  help       = "infer whether in effectively propositional fragment, use for cbqi"
+  help       = "infer whether in effectively propositional fragment, use for cegqi"
 
 [[option]]
   name       = "quantEprMatching"
@@ -1796,7 +1796,7 @@ header = "options/quantifiers_options.h"
   name       = "cegqiBvIneqMode"
   category   = "regular"
   long       = "cegqi-bv-ineq=MODE"
-  type       = "CbqiBvIneqMode"
+  type       = "CegqiBvIneqMode"
   default    = "EQ_BOUNDARY"
   help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
   help_mode  = "Modes for handling bit-vector inequalities in counterexample-guided instantiation."

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index fd06f9be404650c9b41e901a98d5179b83eb3286..f94fee66be388d4ccba92f7b8568aba20d1b1969 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -153,7 +153,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
   {
     return Node::null();
   }
-  else if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::KEEP
+  else if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::KEEP
            || (pol && k == EQUAL))
   {
     return lit;
@@ -172,7 +172,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
   Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
 
   Node ret;
-  if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK)
+  if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::EQ_SLACK)
   {
     // if using slack, we convert constraints to a positive equality based on
     // the current model M, e.g.: