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

fix #5663

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-11-12 11:36:42 -08:00
parent 3c16edc8d3
commit b6f7deacf4
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/opt/optsmt.cpp
View file

@ -305,11 +305,9 @@ namespace opt {
expr_ref fml(m), bound(m.mk_true(), m), tmp(m); expr_ref fml(m), bound(m.mk_true(), m), tmp(m);
expr* vars[1]; expr* vars[1];
{ {
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]));
}
fml = mk_or(ors); fml = mk_or(ors);
tmp = m.mk_fresh_const("b", m.mk_bool_sort()); tmp = m.mk_fresh_const("b", m.mk_bool_sort());
fml = m.mk_implies(tmp, fml); fml = m.mk_implies(tmp, fml);
@ -328,8 +326,7 @@ namespace opt {
m_s->get_model(m_model); m_s->get_model(m_model);
m_s->get_labels(m_labels); m_s->get_labels(m_labels);
for (unsigned i = 0; i < ors.size(); ++i) { for (unsigned i = 0; i < ors.size(); ++i) {
expr_ref tmp(m); if (m_model->is_true(ors.get(i))) {
if (m_model->is_true(ors[i].get())) {
m_lower[i] = m_upper[i]; m_lower[i] = m_upper[i];
ors[i] = m.mk_false(); ors[i] = m.mk_false();
disj[i] = m.mk_false(); disj[i] = m.mk_false();

5
src/smt/theory_lra.cpp
View file

@ -3477,7 +3477,10 @@ public:
st = lp::lp_status::FEASIBLE; st = lp::lp_status::FEASIBLE;
lp().restore_x(); lp().restore_x();
} }
if (m_nla && st == lp::lp_status::OPTIMAL) {
st = lp::lp_status::FEASIBLE;
lp().restore_x();
}
} }
switch (st) { switch (st) {
case lp::lp_status::OPTIMAL: { case lp::lp_status::OPTIMAL: {