From 859013e9c939c7de7080b66790a656ce066c49d8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 22 Apr 2014 19:13:43 +0100 Subject: [PATCH] bvsls opt engine bugfix/debugging Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/bvsls_opt_engine.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp index 12a0cf631..95a9389fc 100644 --- a/src/tactic/sls/bvsls_opt_engine.cpp +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -53,11 +53,14 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize( tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl; }); m_hard_tracker.set_model(initial_model); - } + m_evaluator.update_all(); + } optimization_result res(m_manager); lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef; + TRACE("sls_opt", tout << "initial model is sat? " << is_sat << std::endl;); + for (m_stats.m_restarts = 0; m_stats.m_restarts < m_max_restarts; m_stats.m_restarts++) @@ -65,7 +68,7 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize( mpz old_best; m_mpz_manager.set(old_best, m_best_model_score); - if (!is_sat) { + if (is_sat != l_true) { do { checkpoint();