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

fix build

Browse source
This commit is contained in:
Nuno Lopes 2020-05-10 10:35:46 +01:00
parent 0a6908cd15
commit 6c72f39142
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -330,7 +330,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm
else if (abs(val(j)) != rational(1)) else if (abs(val(j)) != rational(1))
not_one_j = j; not_one_j = j;
} }
if (jl == null_lpvar || not_one_j = null_lpvar) if (jl == null_lpvar || not_one_j == null_lpvar)
return false; return false;
new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1"); new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1");
@ -528,7 +528,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
else if (abs(val(j)) != rational(1)) else if (abs(val(j)) != rational(1))
not_one_j = j; not_one_j = j;
} }
if (jl == null_lpvar || not_one_j = null_lpvar) if (jl == null_lpvar || not_one_j == null_lpvar)
return false; return false;
new_lemma lemma(c(), __FUNCTION__); new_lemma lemma(c(), __FUNCTION__);
@ -628,7 +628,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic
else if (abs(val(fc)) != rational(1)) else if (abs(val(fc)) != rational(1))
not_one_j = j; not_one_j = j;
} }
if (jl == null_lpvar || not_one_j = null_lpvar) if (jl == null_lpvar || not_one_j == null_lpvar)
return false; return false;
new_lemma lemma(c(), __FUNCTION__); new_lemma lemma(c(), __FUNCTION__);