mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix in patching of monics

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-01 12:58:34 -07:00
parent 5e2927aa96
commit 0dc5bad6e4
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1405,7 +1405,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
for (unsigned l = 0; l < m.size(); l++) {
lpvar k = m.vars()[l];
if (!in_power(m.vars(), l) &&
var_is_int(k) &&
!var_is_int(k) &&
!var_is_used_in_a_correct_monic(k) &&
try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k
SASSERT(mul_val(m) == var_val(m));