From f45fcbe2829e152bf35adc6a3b241089a91ded24 Mon Sep 17 00:00:00 2001
From: Aleksandar Zeljic <aleksandar.zeljic@it.uu.se>
Date: Fri, 12 Jun 2015 11:47:58 +0200
Subject: [PATCH] Added support for patching of models containing toIntegral,
 max, min.

---
 src/tactic/fpa/fpa2bv_approx_tactic.cpp | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp
index 77a87ae31..211da9dc7 100644
--- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_approx_tactic.cpp
@@ -384,6 +384,24 @@ class fpa2bv_approx_tactic: public tactic {
                 mpf_mngr.abs(est_arg_val[0], est_rhs_value);
                 break;
             }
+            case OP_FPA_MIN:
+            {
+                mpf_mngr.minimum( arg_val[1], arg_val[2], rhs_value);
+                mpf_mngr.minimum( est_arg_val[1], est_arg_val[2], est_rhs_value);
+                break;
+            }
+            case OP_FPA_MAX:
+            {
+                mpf_mngr.maximum( arg_val[1], arg_val[2], rhs_value);
+                mpf_mngr.maximum( est_arg_val[1], est_arg_val[2], est_rhs_value);
+                break;
+            }
+            case OP_FPA_ROUND_TO_INTEGRAL:
+            {
+                mpf_mngr.round_to_integral(rm,arg_val[1],rhs_value);
+                mpf_mngr.round_to_integral(rm,est_arg_val[1],est_rhs_value);
+                break;
+            }
             default:
                 NOT_IMPLEMENTED_YET();
                 break;