mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 01:32:17 +00:00
Code Activity

cosmetics

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-25 10:58:05 -10:00
parent 3271f2fad9
commit 8850ea6cab
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/dioph_eq.cpp
View file

@ -1480,9 +1480,7 @@ namespace lp {
lia_move tighten_bounds_for_term_column(unsigned j) { lia_move tighten_bounds_for_term_column(unsigned j) {
term_o term_to_tighten = lra.get_term(j); // copy the term aside term_o term_to_tighten = lra.get_term(j); // copy the term aside
SASSERT(get_extended_term_value(term_to_tighten).is_zero()); SASSERT(get_extended_term_value(term_to_tighten).is_zero() && all_vars_are_int(term_to_tighten));
if (!all_vars_are_int(term_to_tighten))
return lia_move::undef;
// q is the queue of variables that can be substituted in term_to_tighten // q is the queue of variables that can be substituted in term_to_tighten
protected_queue q; protected_queue q;
TRACE("dio", tout << "j:" << j << ", t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;); TRACE("dio", tout << "j:" << j << ", t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;);
@ -1706,7 +1704,8 @@ namespace lp {
SASSERT(!g.is_zero()); SASSERT(!g.is_zero());
if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) { if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) {
TRACE("dio", tout << "current upper bound for x" << j << ":" TRACE("dio",
tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":"
<< rs << std::endl;); << rs << std::endl;);
rs = (rs - m_c) / g; rs = (rs - m_c) / g;
TRACE("dio", tout << "(rs - m_c) / g:" << rs << std::endl;); TRACE("dio", tout << "(rs - m_c) / g:" << rs << std::endl;);