mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

initialize best model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-28 12:31:13 -03:00
parent 20dc59e02d
commit 35fa24a82a
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/opt/optsmt.cpp
View file

@ -498,6 +498,7 @@ namespace opt {
lbool optsmt::lex(unsigned obj_index, bool is_maximize) { lbool optsmt::lex(unsigned obj_index, bool is_maximize) {
TRACE("opt", tout << "optsmt:lex\n";); TRACE("opt", tout << "optsmt:lex\n";);
m_context.get_base_model(m_best_model);
solver::scoped_push _push(*m_s); solver::scoped_push _push(*m_s);
SASSERT(obj_index < m_vars.size()); SASSERT(obj_index < m_vars.size());
if (is_maximize && m_optsmt_engine == symbol("farkas")) { if (is_maximize && m_optsmt_engine == symbol("farkas")) {