mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

fpa2bv_approx: bugfix for fp.abs

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-02 18:40:11 +01:00
parent a93bb92240
commit c910ed2eae
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/fpa/fpa2bv_approx_tactic.cpp
View file

@ -379,6 +379,7 @@ class fpa2bv_approx_tactic: public tactic {
case OP_FPA_ABS: case OP_FPA_ABS:
{ {
mpf_mngr.abs(arg_val[0], rhs_value); mpf_mngr.abs(arg_val[0], rhs_value);
mpf_mngr.abs(est_arg_val[0], est_rhs_value);
break; break;
} }
default: default: