From bb6813731ef1059ab38cedcc5af026b6e75bd6be Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 14 Jul 2021 18:54:33 -0700 Subject: bv: Rename lazy solver to layered solver. (#6889) --- test/unit/theory/theory_bv_white.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'test') diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 150320824..4cf695609 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -22,7 +22,7 @@ #include "expr/node.h" #include "test_smt.h" #include "theory/bv/bitblast/eager_bitblaster.h" -#include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_layered.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -45,7 +45,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) d_smtEngine->setLogic("QF_BV"); d_smtEngine->setOption("bitblast", "eager"); - d_smtEngine->setOption("bv-solver", "lazy"); + d_smtEngine->setOption("bv-solver", "layered"); d_smtEngine->setOption("incremental", "false"); // Notice that this unit test uses the theory engine of a created SMT // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized @@ -53,7 +53,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) d_smtEngine->finishInit(); TheoryBV* tbv = dynamic_cast( d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]); - BVSolverLazy* bvsl = dynamic_cast(tbv->d_internal.get()); + BVSolverLayered* bvsl = dynamic_cast(tbv->d_internal.get()); std::unique_ptr bb( new EagerBitblaster(bvsl, d_smtEngine->getContext())); -- cgit v1.2.3