mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
1603075189
commit
d400929d9a
|
@ -503,7 +503,7 @@ namespace smt {
|
|||
tout << "lower: " << lower << "\n";
|
||||
tout << "upper: " << upper << "\n";);
|
||||
|
||||
mk_axiom(eqz, eq, true);
|
||||
mk_axiom(eqz, eq, false);
|
||||
mk_axiom(eqz, lower, false);
|
||||
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
|
||||
rational k;
|
||||
|
|
Loading…
Reference in a new issue