mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add an assert

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-01 10:44:15 -07:00
parent c76adfaf19
commit c4416f822e
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -1374,6 +1374,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
if (!var_is_int(j) && if (!var_is_int(j) &&
!var_is_used_in_a_correct_monic(j) !var_is_used_in_a_correct_monic(j)
&& try_to_patch(j, v)) { && try_to_patch(j, v)) {
SASSERT(v == val(j));
m_to_refine.erase(j); m_to_refine.erase(j);
} else { } else {
rational r = val(j) / v; rational r = val(j) / v;
@ -1383,6 +1384,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
continue; continue;
if (try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k if (try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
m_to_refine.erase(j); m_to_refine.erase(j);
SASSERT(mul_val(m) == val(j));
break; break;
} }
} }