mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

add model on unknown, to address issue #139

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-06-23 14:45:52 +02:00 • committed by Christoph M. Wintersteiger
parent 3de2a70a48
commit cd05edf833
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/opt/opt_context.cpp
View file

@ -225,12 +225,13 @@ namespace opt {
IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
lbool is_sat = s.check_sat(0,0); lbool is_sat = s.check_sat(0,0);
TRACE("opt", tout << "initial search result: " << is_sat << "\n";); TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
if (is_sat != l_false) {
s.get_model(m_model);
}
if (is_sat != l_true) { if (is_sat != l_true) {
m_model = 0;
return is_sat; return is_sat;
} }
IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";); IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
s.get_model(m_model);
TRACE("opt", model_smt2_pp(tout, m, *m_model, 0);); TRACE("opt", model_smt2_pp(tout, m, *m_model, 0););
m_optsmt.setup(*m_opt_solver.get()); m_optsmt.setup(*m_opt_solver.get());
update_lower(); update_lower();