From b96e203aea67ba62b2ca8a32da965bff652bb401 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 13 Feb 2020 13:53:26 -1000
Subject: [PATCH] fix #2989

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_arith_plugin.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index a09c4046e..f72c9fbe1 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -1022,7 +1022,10 @@ namespace qe {
             //
             // The first entry in values is the constant.
             //
-            VERIFY(m_arith_solver.solve_integer_equation(values, index, is_aux));
+            if (!m_arith_solver.solve_integer_equation(values, index, is_aux)) {
+                // equation is unsat
+                return false;
+            }
 
             SASSERT(1 <= index && index <= num_vars);
             app_ref x(m_ctx.get_var(index-1), m);