From a8b47b4fb225d372059ed01562eac808afdc4bcd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Sep 2015 14:47:35 +0200
Subject: [PATCH] enable coercions when interpolation creates MILP constraints.
 Issue #217

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/interp/iz3translate.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index b4cd22830..51084f809 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1407,6 +1407,7 @@ public:
 
         hash_map<ast,ast> dual_map;
         std::vector<ast> cvec, vars_seen;
+        m().enable_int_real_coercions(true);
         ast rhs = make_real(rational(0));
         for(unsigned i = 0; i < npcons.size(); i++){
             ast c= mk_fresh_constant("@c",real_type());