From 1741671a9cacf7ccc195e5f4232bc6899f9f3c4e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Sep 2013 13:32:35 -0700
Subject: [PATCH] update test in qe_arith

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

diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 393467cc7..b4f1a781a 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -168,7 +168,7 @@ namespace qe {
         unsigned find_max(model& mdl, bool do_pos) {
             unsigned result;
             bool found = false;
-            rational found_val(0), r;
+            rational found_val(0), r, found_c;
             expr_ref val(m);
             for (unsigned i = 0; i < m_ineq_terms.size(); ++i) {
                 rational const& ac = m_ineq_coeffs[i];
@@ -180,11 +180,15 @@ namespace qe {
                     if (!found || r > found_val) {
                         result = i;
                         found_val = r;
+                        found_c = ac;
                         found = true;
                     }
                 }
             }
             SASSERT(found);
+            if (a.is_int(m_var->x()) && !found_c.is_one()) {
+                throw cant_project();
+            }
             return result;
         }