mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #6391
This commit is contained in:
parent
a41520acf1
commit
ace727ee0f
|
@ -1775,7 +1775,6 @@ public:
|
|||
hi = floor(hi/mul);
|
||||
lo = ceil(lo/mul);
|
||||
}
|
||||
std::cout << mk_pp(p, m) << " " << mk_pp(n, m) << " " << hi << " " << lo << " " << div_r << "\n";
|
||||
literal p_le_r1 = mk_literal(a.mk_le(p, a.mk_numeral(hi, true)));
|
||||
literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
|
||||
literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
|
||||
|
|
Loading…
Reference in a new issue