From f86205b0e83ad587ed5e188ed2c1692d8ecc4bfe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Mar 2020 12:24:22 -0700
Subject: [PATCH] fix #3343

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_farkas_util.cpp | 12 +++++++++---
 src/smt/smt_farkas_util.h   |  3 ++-
 src/smt/theory_arith_aux.h  |  7 +++++--
 3 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/smt/smt_farkas_util.cpp b/src/smt/smt_farkas_util.cpp
index f7aaea61b..e427c9224 100644
--- a/src/smt/smt_farkas_util.cpp
+++ b/src/smt/smt_farkas_util.cpp
@@ -297,7 +297,7 @@ namespace smt {
         m_coeffs.reset();        
     }
     
-    void farkas_util::add(rational const & coef, app * c) {
+    bool farkas_util::add(rational const & coef, app * c) {
         bool is_pos = true;
         expr* e;
         while (m.is_not(c, e)) {
@@ -306,9 +306,15 @@ namespace smt {
         }
         
         if (!coef.is_zero() && !m.is_true(c)) {
-            m_coeffs.push_back(coef);                
-            m_ineqs.push_back(fix_sign(is_pos, c));                
+            if (m.is_eq(c) || a.is_le(c) || a.is_lt(c) || a.is_gt(c) || a.is_ge(c)) {
+                m_coeffs.push_back(coef);
+                m_ineqs.push_back(fix_sign(is_pos, c));
+            }
+            else {
+                return false;
+            }
         }
+        return true;
     }
     
     expr_ref farkas_util::get() {
diff --git a/src/smt/smt_farkas_util.h b/src/smt/smt_farkas_util.h
index 1fc6a3681..73f7ff388 100644
--- a/src/smt/smt_farkas_util.h
+++ b/src/smt/smt_farkas_util.h
@@ -67,8 +67,9 @@ namespace smt {
 
         /** 
             \brief add a multiple of constraint c to the current state 
+            Fail if the constraint cannot be classified.
          */
-        void add(rational const & coef, app * c);
+        bool add(rational const & coef, app * c);
 
         /**
            \brief Extract the complement of premises multiplied by Farkas coefficients.
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index e8501e4cd..fb6ebb992 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1227,7 +1227,8 @@ namespace smt {
                 continue;
             }
             ctx.literal2expr(lits[i], tmp);
-            farkas.add(abs(pa.get_rational()), to_app(tmp));
+            if (!farkas.add(abs(pa.get_rational()), to_app(tmp)))
+                return;
         }
         for (unsigned i = 0; i < num_eqs; ++i) {
             enode_pair const& p = eqs[i];
@@ -1236,9 +1237,11 @@ namespace smt {
             tmp = m.mk_eq(x,y);
             parameter const& pa = params[1 + num_lits + i];
             SASSERT(pa.is_rational());
-            farkas.add(abs(pa.get_rational()), to_app(tmp));
+            if (!farkas.add(abs(pa.get_rational()), to_app(tmp)))
+                return;
         }
         tmp = farkas.get();
+
         if (m.has_trace_stream()) {
             log_axiom_instantiation(tmp);
             m.trace_stream() << "[end-of-instance]\n";