mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 14:55:25 +00:00
Code Activity

rename 'or' to 'fml' toe mae gcc happy, reported by Geroge Karpenkov

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-11-25 10:23:41 -08:00
parent 2dccfc0ce2
commit e9baaa0900
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/opt/optsmt.cpp
View file

@ -124,14 +124,14 @@ namespace opt {
expr_ref_vector ors(m), disj(m); expr_ref_vector ors(m), disj(m);
expr_ref or(m), bound(m.mk_true(), m); expr_ref fml(m), bound(m.mk_true(), m);
for (unsigned i = 0; i < m_upper.size(); ++i) { for (unsigned i = 0; i < m_upper.size(); ++i) {
ors.push_back(m_s->mk_ge(i, m_upper[i])); ors.push_back(m_s->mk_ge(i, m_upper[i]));
} }
{ {
solver::scoped_push _push(*m_s); solver::scoped_push _push(*m_s);
or = m.mk_or(ors.size(), ors.c_ptr()); fml = m.mk_or(ors.size(), ors.c_ptr());
m_s->assert_expr(or); m_s->assert_expr(fml);
lbool is_sat = l_true; lbool is_sat = l_true;
while (!m_cancel) { while (!m_cancel) {
is_sat = m_s->check_sat(0,0); is_sat = m_s->check_sat(0,0);
@ -149,8 +149,8 @@ namespace opt {
} }
} }
set_max(m_lower, m_s->get_objective_values(), disj); set_max(m_lower, m_s->get_objective_values(), disj);
or = m.mk_or(ors.size(), ors.c_ptr()); fml = m.mk_or(ors.size(), ors.c_ptr());
m_s->assert_expr(or); m_s->assert_expr(fml);
} }
else if (is_sat == l_undef) { else if (is_sat == l_undef) {
return l_undef; return l_undef;