From f330b96a3555b485a12acfc5c3a2f597b4c4313a Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Sun, 24 Jun 2018 21:03:09 -0400
Subject: [PATCH] Gracefully failing in assign-bounds to farkas

---
 src/muz/spacer/spacer_proof_utils.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp
index ea91a7d04..dc3bbf30c 100644
--- a/src/muz/spacer/spacer_proof_utils.cpp
+++ b/src/muz/spacer/spacer_proof_utils.cpp
@@ -307,7 +307,10 @@ namespace spacer {
 
         rational rat1, rat2, coeff0;
         arith_util a(m);
-        if (a.is_numeral(val1, rat1) && a.is_numeral(val2, rat2)) {
+        CTRACE("spacer.fkab", !(val1 && val2),
+               tout << "Failed to match variables\n";);
+        if (val1 && val2 &&
+            a.is_numeral(val1, rat1) && a.is_numeral(val2, rat2)) {
             coeff0 = abs(rat2/rat1);
             coeff0 = coeff0 / lcb.lc();
             TRACE("spacer.fkab", tout << "coeff0: " << coeff0 << "\n";);