mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #1645

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-24 09:21:20 -07:00
parent 2e4fb8d356
commit 6ecae2b986
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/opt/opt_context.cpp
View file

@ -319,8 +319,7 @@ namespace opt {
is_sat = execute_box(); is_sat = execute_box();
} }
else { else {
m_pareto1 = (pri == symbol("pareto")); is_sat = execute_lex();
is_sat = execute(m_objectives[0], true, false);
} }
} }
} }
@ -425,7 +424,10 @@ namespace opt {
objective const& o = m_objectives[i]; objective const& o = m_objectives[i];
bool is_last = i + 1 == sz; bool is_last = i + 1 == sz;
r = execute(o, i + 1 < sz, sc && !is_last && o.m_type != O_MAXSMT); r = execute(o, i + 1 < sz, sc && !is_last && o.m_type != O_MAXSMT);
if (r == l_true && !get_lower_as_num(i).is_finite()) { if (r == l_true && o.m_type == O_MINIMIZE && !get_lower_as_num(i).is_finite()) {
return r;
}
if (r == l_true && o.m_type == O_MAXIMIZE && !get_upper_as_num(i).is_finite()) {
return r; return r;
} }
if (r == l_true && i + 1 < sz) { if (r == l_true && i + 1 < sz) {