diff options
Diffstat (limited to 'src/prop/bvminisat/core/Solver.cc')
| -rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 3b2b814cd..d7dc3f6d4 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -34,7 +34,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "theory/interrupted.h" #include "util/utility.h" -namespace CVC4 { +namespace CVC5 { namespace BVMinisat { #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] " @@ -82,7 +82,7 @@ CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here //================================================================================================= // Constructor/Destructor: -Solver::Solver(CVC4::context::Context* context) +Solver::Solver(CVC5::context::Context* context) : // Parameters (user settable): @@ -976,7 +976,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) return l_False; } - if (!CVC4::options::bvEagerExplanations()) + if (!CVC5::options::bvEagerExplanations()) { // check if uip leads to a conflict if (backtrack_level < assumptions.size()) @@ -1028,7 +1028,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) isWithinBudget = withinBudget(ResourceManager::Resource::BvSatConflictsStep); } - catch (const CVC4::theory::Interrupted& e) + catch (const CVC5::theory::Interrupted& e) { // do some clean-up and rethrow cancelUntil(assumptions.size()); @@ -1417,5 +1417,5 @@ bool Solver::withinBudget(ResourceManager::Resource r) const propagations < (uint64_t)propagation_budget); } -} /* CVC4::BVMinisat namespace */ -} /* CVC4 namespace */ +} // namespace BVMinisat +} // namespace CVC5 |