From 33f941aaec11bf7ef754d5779e581ba4a26b3018 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Nov 2013 12:20:55 -0800
Subject: [PATCH] interpolation fix

---
 src/interp/iz3mgr.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 75948f348..2a15408f3 100644
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -594,6 +594,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa
     }
     rats[i-1] = r;
   }
+#if 0
   if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them
     for(unsigned i = 1; i < rats.size(); i++){
       if(!rats[i].is_neg())
@@ -601,6 +602,8 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa
       rats[i] = -rats[i];
     }
   }
+#endif
+  abs_rat(rats);
   extract_lcd(rats);
 }