mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

compilation fix

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-04-25 18:58:19 +01:00
parent 8fe2db1eed
commit 5fab191c6c
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -16,7 +16,6 @@ Author:
Notes: Notes:
--*/ --*/
#include "sls_compilation_settings.h"
#include "nnf.h" #include "nnf.h"
#include "bvsls_opt_engine.h" #include "bvsls_opt_engine.h"
@ -42,7 +41,6 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " << TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " <<
mk_ismt2_pp(objective, m()) << std::endl;); mk_ismt2_pp(objective, m()) << std::endl;);
m_hard_tracker.initialize(m_assertions); m_hard_tracker.initialize(m_assertions);
m_restart_limit = _RESTART_LIMIT_;
setup_opt_tracker(objective, _maximize); setup_opt_tracker(objective, _maximize);
if (initial_model.get() != 0) { if (initial_model.get() != 0) {
@ -53,7 +51,7 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl; tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl;
}); });
m_hard_tracker.set_model(initial_model); m_hard_tracker.set_model(initial_model);
m_evaluator.update_all(); m_evaluator.update_all();
} }
optimization_result res(m_manager); optimization_result res(m_manager);