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

#5445

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-03 11:17:23 -07:00
parent 60a25053c6
commit 202ed79a24
3 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/simplex/model_based_opt.cpp
View file

@ -1227,6 +1227,8 @@ namespace opt {
if (m_var2is_int[x] && !a.is_one()) { if (m_var2is_int[x] && !a.is_one()) {
row& r1 = m_rows[row_id1]; row& r1 = m_rows[row_id1];
r1.m_coeff -= r1.m_value;
r1.m_value = 0;
vector<var> coeffs; vector<var> coeffs;
mk_coeffs_without(coeffs, r1.m_vars, x); mk_coeffs_without(coeffs, r1.m_vars, x);
rational c = mod(-eval(coeffs), a); rational c = mod(-eval(coeffs), a);

9
src/sat/smt/euf_solver.cpp
View file

@ -315,14 +315,11 @@ namespace euf {
m_egraph.merge(n, nb, c); m_egraph.merge(n, nb, c);
} }
if (n->is_equality()) { if (n->is_equality()) {
SASSERT(!m.is_iff(e));
if (sign) if (sign)
m_egraph.new_diseq(n); m_egraph.new_diseq(n);
else { else
SASSERT(!m.is_iff(e)); m_egraph.merge(n->get_arg(0), n->get_arg(1), c);
euf::enode* na = n->get_arg(0);
euf::enode* nb = n->get_arg(1);
m_egraph.merge(na, nb, c);
}
} }
} }

4
src/util/sexpr.cpp
View file

@ -185,8 +185,10 @@ void sexpr::display_atom(std::ostream & out) const {
} }
void sexpr::display(std::ostream & out) const { void sexpr::display(std::ostream & out) const {
if (!is_composite()) if (!is_composite()) {
display_atom(out); display_atom(out);
return;
}
vector<std::pair<sexpr_composite const *, unsigned> > todo; vector<std::pair<sexpr_composite const *, unsigned> > todo;
todo.push_back(std::make_pair(static_cast<sexpr_composite const *>(this), 0)); todo.push_back(std::make_pair(static_cast<sexpr_composite const *>(this), 0));
while (!todo.empty()) { while (!todo.empty()) {