From 1a70fce92eb127480a79eaf8af7dc19d089cfd5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jul 2019 08:45:51 -0700 Subject: [PATCH] add back nvars Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1978f967e..747adbc68 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2196,7 +2196,7 @@ namespace sat { void solver::update_activity(bool_var v, double p) { unsigned old_act = m_activity[v]; - unsigned new_act = (unsigned) (m_config.m_activity_scale * p); + unsigned new_act = (unsigned) (num_vars() * m_config.m_activity_scale * p); m_activity[v] = new_act; if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) { m_case_split_queue.activity_changed_eh(v, new_act > old_act);