Properly set up equality engine for BV bitblast solver. (#5905)

[cvc5.git] / src / theory / bv / bv_subtheory_core.cpp

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 87cc0bc4de76d7b31b537924d02ae009e4602ef0..b839066888b0414dbfcdf4b28de093506d2db48f 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -188,8 +188,7 @@ void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
 
-  d_bv->d_inferManager.spendResource(
-      ResourceManager::Resource::TheoryCheckStep);
+  d_bv->d_im.spendResource(ResourceManager::Resource::TheoryCheckStep);
 
   d_checkCalled = true;
   Assert(!d_bv->inConflict());
@@ -560,7 +559,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
                               nm->mkNode(kind::LT, n, max));
         Trace("bv-extf-lemma")
             << "BV extf lemma (range) : " << lem << std::endl;
-        d_bv->d_inferManager.lemma(lem, InferenceId::UNKNOWN);
+        d_bv->d_im.lemma(lem, InferenceId::UNKNOWN);
         sentLemma = true;
       }
     }
@@ -609,7 +608,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
           //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
           Trace("bv-extf-lemma")
               << "BV extf lemma (collapse) : " << lem << std::endl;
-          d_bv->d_inferManager.lemma(lem, InferenceId::UNKNOWN);
+          d_bv->d_im.lemma(lem, InferenceId::UNKNOWN);
           sentLemma = true;
         }
       }