diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp
index 9d5873f12..bc0b5d39a 100644
--- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_approx_tactic.cpp
@@ -272,8 +272,12 @@ class fpa2bv_approx_tactic: public tactic {
             expr_ref arg_e[] = { expr_ref(m), expr_ref(m), expr_ref(m), expr_ref(m) };
             unsigned i=0;
             //Set rounding mode
-            if (rhs->get_num_args() > 0 && m_float_util.is_rm(rhs->get_arg(0)))
+            if (rhs->get_num_args() > 0 && m_float_util.is_rm(rhs->get_arg(0))) {
+                expr_ref rm_val(m);
+                mdl->eval(rhs->get_arg(0), rm_val, true);
+                m_float_util.is_rm_numeral(rm_val, rm);
                 i = 1;
+            }
             //Collect argument values
             for (; i < rhs->get_num_args(); i++) {
                 expr * arg = rhs->get_arg(i);
@@ -372,6 +376,11 @@ class fpa2bv_approx_tactic: public tactic {
                 mpf_mngr.set(est_rhs_value, ebits, sbits, rm, est_arg_val[1]);
                 break;
             }
+            case OP_FPA_ABS:
+            {
+                mpf_mngr.abs(arg_val[0], rhs_value);
+                break;
+            }
             default:
                 NOT_IMPLEMENTED_YET();
                 break;