mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
85da7407dc
commit
af5fd1014f
|
@ -418,6 +418,7 @@ namespace arith {
|
|||
expr* p = nullptr, * q = nullptr;
|
||||
VERIFY(a.is_idiv(n, p, q));
|
||||
theory_var v1 = internalize_def(p);
|
||||
ensure_column(v1);
|
||||
lp::impq r1 = get_ivalue(v1);
|
||||
rational r2;
|
||||
|
||||
|
|
Loading…
Reference in a new issue