From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 20 May 2020 07:08:43 +0000 (-0700)
Subject: CegqiBv: Clean up after renaming options. (#4487)
X-Git-Tag: cvc5-1.0.0~3311
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3620b97ea7fac5dd16f5bd99f8dd10226c60d92;p=cvc5.git

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

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 21cba6abb..1834c90c4 100644
--- 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 fd06f9be4..f94fee66b 100644
--- 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.: