From 95146483eaace2638eb6916af490184cc2342494 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 13 May 2014 18:15:51 -0700
Subject: [PATCH] add round-off to farkas resconstruction in interp

---
 src/interp/iz3translate.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index e467da1fc..26786d57a 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1364,8 +1364,13 @@ public:
     int nprems = prems.size();
     std::vector<ast> npcons(nprems);
     hash_map<ast,ast> pain_map; // not needed
-    for(int i = 0; i < nprems; i++)
+    for(int i = 0; i < nprems; i++){
       npcons[i] = painfully_normalize_ineq(conc(prems[i]),pain_map);
+      if(op(npcons[i]) == Lt){
+	ast constval = z3_simplify(make(Sub,arg(npcons[i],1),make_int(rational(1))));
+	npcons[i] = make(Leq,arg(npcons[i],0),constval);
+      }
+    }
     ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
     npcons.push_back(ncon);