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

null

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-09 21:27:45 -07:00
parent 30de76b529
commit 086331a24b
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -321,7 +321,8 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm
lpvar jl = null_lpvar; lpvar jl = null_lpvar;
for (auto fc : f ) { for (auto fc : f ) {
lpvar j = var(fc); lpvar j = var(fc);
if (abs(val(j)) == abs_mv && c().vars_are_equiv(j, mon_var) && if (j == null_lpvar && abs(val(j)) == abs_mv &&
c().vars_are_equiv(j, mon_var) &&
(mon_var_is_sep_from_zero || c().var_is_separated_from_zero(j))) { (mon_var_is_sep_from_zero || c().var_is_separated_from_zero(j))) {
jl = j; jl = j;
} }
@ -533,7 +534,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
} }
lpvar jl = null_lpvar; lpvar jl = null_lpvar;
for (auto j : m.vars() ) { for (auto j : m.vars() ) {
if (abs(val(j)) == abs_mv) { if (jl == null_lpvar && abs(val(j)) == abs_mv) {
jl = j; jl = j;
} }
else if (jl == j) else if (jl == j)
@ -645,7 +646,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic
lpvar jl = null_lpvar; lpvar jl = null_lpvar;
for (auto fc : f) { for (auto fc : f) {
lpvar j = var(fc); lpvar j = var(fc);
if (abs(val(fc)) == abs_mv) { if (j == null_lpvar && abs(val(fc)) == abs_mv) {
jl = j; jl = j;
} }
else if (j == jl) else if (j == jl)