From dd5e2e8930fc1b91c4faa850168d5d7763bdd34b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jul 2020 10:43:50 -0700 Subject: [PATCH] check for 0 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.mli | 3 +++ src/sat/sat_solver.cpp | 3 ++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 6b797c552..252cabb7b 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2862,6 +2862,9 @@ sig val get_decls : model -> FuncDecl.func_decl list (** Evaluates an expression in the current model. + The Boolean argument indicates whether to apply model completion. + When model completion is true it will assign an interpretation for + constants and functions that do not have an interpretation in the model. This function may fail if the argument contains quantifiers, is partial (MODEL_PARTIAL enabled), or if it is not well-sorted. diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a788f7ee7..7834f0541 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3974,7 +3974,8 @@ namespace sat { double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0); for (unsigned i = qhead; i < m_trail.size(); ++i) { auto v = m_trail[i].var(); - auto reward = multiplier / (m_stats.m_conflict - m_last_conflict[v] + 1); + auto d = std::max(1ull,m_stats.m_conflict - m_last_conflict[v] + 1); + auto reward = multiplier / d; auto activity = m_activity[v]; set_activity(v, static_cast(m_step_size * reward + ((1.0 - m_step_size) * activity))); }