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

fix the build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-12 15:31:56 -08:00
parent 1b07ad0952
commit 8980aff7f3
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/nex_creator.cpp
View file

@ -531,7 +531,6 @@ nex * nex_creator::mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b) {
}
nex * nex_creator::mk_div_by_mul(const nex& a, const nex_mul& b) {
SASSERT(have_no_scalars(b));
SASSERT(!a.is_var() || (b.get_degree() == 1 && get_vars_of_expr(&a) == get_vars_of_expr(&b) && b.coeff().is_one()));
if (a.is_sum()) {
return mk_div_sum_by_mul(a.to_sum(), b);