From caa616f11b93a3175abef079f1f35e684e4446e9 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 20 May 2015 15:37:51 -0700
Subject: [PATCH] fix for github issue 83

---
 src/interp/iz3mgr.cpp       | 14 ++++++++++++++
 src/interp/iz3mgr.h         |  2 ++
 src/interp/iz3translate.cpp |  8 +++++++-
 3 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 5a7f71987..78dd6f174 100755
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -556,6 +556,20 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
     extract_lcd(rats);
 }
 
+void iz3mgr::get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats){
+    symb s = sym(proof);
+    int numps = s->get_num_parameters();
+    rats.resize(numps-2);
+    for(int i = 2; i < numps; i++){
+        rational r;
+        bool ok = s->get_parameter(i).is_rational(r);
+        if(!ok)
+            throw "Bad Farkas coefficient";
+        rats[i-2] = r;
+    }
+    extract_lcd(rats);
+}
+
 void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& coeffs){
     std::vector<rational> rats;
     get_assign_bounds_coeffs(proof,rats);
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 54fb35a0f..8d4479f8f 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -424,6 +424,8 @@ class iz3mgr  {
 
     void get_farkas_coeffs(const ast &proof, std::vector<rational>& rats);
 
+    void get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats);
+
     void get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats);
 
     void get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& rats);
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index d1479e4cc..f510f4070 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1021,6 +1021,12 @@ public:
                 my_coeffs.push_back(make_int(c));
                 my_prem_cons.push_back(conc(prem(proof,i)));
             }
+            else if(c.is_neg()){
+                int j = (i % 2 == 0) ? i + 1 : i - 1;
+                my_prems.push_back(prems[j]);
+                my_coeffs.push_back(make_int(-coeffs[j]));
+                my_prem_cons.push_back(conc(prem(proof,j)));
+            }
         }
         ast my_con = sum_inequalities(my_coeffs,my_prem_cons);
 
@@ -1884,7 +1890,7 @@ public:
                     }
                     case GCDTestKind: {
                         std::vector<rational> farkas_coeffs;
-                        get_farkas_coeffs(proof,farkas_coeffs);
+                        get_broken_gcd_test_coeffs(proof,farkas_coeffs);
                         if(farkas_coeffs.size() != nprems){
                             pfgoto(proof);
                             throw unsupported();