From 55cb12e23387239c7314bebb74d185b20ef506bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 8 Feb 2021 16:53:30 -0800 Subject: [PATCH] build fix --- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/sat/smt/bv_solver.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 65a096b20..4e17ec4d8 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -315,7 +315,7 @@ public: m_solver.set_phase(lit); } void move_to_front(expr* e) override { - bool is_not = m.is_not(e, e); + m.is_not(e, e); sat::bool_var b = m_map.to_bool_var(e); if (b != sat::null_bool_var) m_solver.move_to_front(b); diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 878ecbe66..2905d79d1 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -31,7 +31,7 @@ namespace bv { public: bit_trail(solver& s, var_pos vp) : s(s), vp(vp), lit(s.m_bits[vp.first][vp.second]) {} - virtual void undo(euf::solver& euf) { + void undo() override { s.m_bits[vp.first][vp.second] = lit; } }; @@ -43,7 +43,7 @@ namespace bv { public: bit_occs_trail(solver& s, atom& a): a(a), m_occs(a.m_occs) {} - virtual void undo() { + void undo() override { a.m_occs = m_occs; } };