From 39f73fa5951e69cb93807578756a8a451fac6866 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Feb 2019 16:56:55 -0800 Subject: [PATCH] ensure that activity works for sat solver from cold state Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 5 +++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d917d1ae6..b933b6ddb 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1656,6 +1656,7 @@ namespace sat { m_min_core.reset(); m_simplifier.init_search(); TRACE("sat", display(tout);); + } /** diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 8a0747d15..9ca1150a9 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -345,9 +345,10 @@ public: m.is_not(var, var); sat::bool_var v = m_map.to_bool_var(var); if (v == sat::null_bool_var) { - throw default_exception("literal does not correspond to a Boolean variable"); + v = m_solver.add_var(true); + m_map.insert(var, v); } - m_solver.set_activity(v, activity); + m_solver.set_activity(v, static_cast(activity)); } proof * get_proof() override {