mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix #5435
This commit is contained in:
parent
2f49094d49
commit
7cb4932ae8
|
@ -1879,11 +1879,13 @@ namespace z3 {
|
|||
Z3_ast r;
|
||||
if (a.is_int()) {
|
||||
expr zero = a.ctx().int_val(0);
|
||||
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
|
||||
expr ge = a >= zero;
|
||||
r = Z3_mk_ite(a.ctx(), ge, a, zero), a, -a);
|
||||
}
|
||||
else if (a.is_real()) {
|
||||
expr zero = a.ctx().real_val(0);
|
||||
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
|
||||
expr ge = a >= zero;
|
||||
r = Z3_mk_ite(a.ctx(), ge, a, -a);
|
||||
}
|
||||
else {
|
||||
r = Z3_mk_fpa_abs(a.ctx(), a);
|
||||
|
|
Loading…
Reference in a new issue