mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity

display

Browse source
This commit is contained in:
Jakob Rath 2023-12-22 11:03:08 +01:00
parent 4dc77036a6
commit 0e8de50d61
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/viable.cpp
View file

@ -2232,16 +2232,20 @@ namespace polysat {
rational const& q_ = e->interval.lo().val();
rational const& r = e->interval.hi_val();
rational const& s_ = e->interval.hi().val();
out << "[ ";
out << "diseq [ ";
out << val_pp(m, p, true) << "*v" << v << " + " << val_pp(m, q_);
out << (e->src[0].is_positive() ? " > " : " >= ");
out << val_pp(m, r, true) << "*v" << v << " + " << val_pp(m, s_);
out << " ] ";
}
else if (e->interval.is_full())
out << "full: " << e->interval << " ";
else if (e->coeff != 1)
out << e->coeff << " * v" << v << " " << e->interval << " ";
else
out << e->interval << " ";
if (e->refined)
out << "refined ";
if (e->side_cond.size() <= 5)
out << e->side_cond << " ";
else