mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

bvsls opt engine bugfix/debugging

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-04-22 19:13:43 +01:00
parent d67b5226f0
commit 859013e9c9
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tactic/sls/bvsls_opt_engine.cpp
View file

@ -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();