From cf176af48e403a15cca38c4f42d3e20458086eba Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Thu, 7 Nov 2013 15:40:44 -0800
Subject: [PATCH] looking for more farkas rules in interpolation

---
 src/interp/iz3mgr.cpp       | 5 +++++
 src/interp/iz3translate.cpp | 8 ++++++++
 2 files changed, 13 insertions(+)

diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 2a15408f3..9ef2fa9ab 100644
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -489,11 +489,15 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
   symb s = sym(proof);
   int numps = s->get_num_parameters();
   rats.resize(numps-2);
+  if(num_prems(proof) < numps-2){
+    std::cout << "bad farkas rule: " << num_prems(proof) << " premises should be " << numps-2 << "\n";
+  }
   for(int i = 2; i < numps; i++){
     rational r;
     bool ok = s->get_parameter(i).is_rational(r);
     if(!ok)
       throw "Bad Farkas coefficient";
+#if 0 
     {
       ast con = conc(prem(proof,i-2));
       ast temp = make_real(r); // for debugging
@@ -501,6 +505,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
       if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
 	r = -r;
     }
+#endif
     rats[i-2] = r;
   }
 #if 0
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 5dc02d1fc..4feb35faa 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1253,6 +1253,10 @@ public:
 	  case FarkasKind: {
 	    std::vector<ast> farkas_coeffs, prem_cons;
 	    get_farkas_coeffs(proof,farkas_coeffs);
+	    if(farkas_coeffs.size() != nprems){
+	      pfgoto(proof);
+	      throw unsupported();
+	    }
 	    prem_cons.resize(nprems);
 	    for(unsigned i = 0; i < nprems; i++)
 	      prem_cons[i] = conc(prem(proof,i));
@@ -1279,6 +1283,10 @@ public:
 	  case GCDTestKind: {
 	    std::vector<rational> farkas_coeffs;
 	    get_farkas_coeffs(proof,farkas_coeffs);
+	    if(farkas_coeffs.size() != nprems){
+	      pfgoto(proof);
+	      throw unsupported();
+	    }
 	    std::vector<Iproof::node> my_prems; my_prems.resize(2);
 	    std::vector<ast> my_prem_cons; my_prem_cons.resize(2);
 	    std::vector<ast> my_farkas_coeffs; my_farkas_coeffs.resize(2);