From 6c67654e64a108fd84ad32481a80ffc0aa289a8a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Mar 2020 09:12:43 -0700
Subject: [PATCH] fix #3335

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_aux.h | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index cf073c039..5818eab3a 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1274,8 +1274,7 @@ namespace smt {
         }
         th_rewriter rw(m);
         rw(vq, tmp);
-        VERIFY(m_util.is_numeral(tmp, q));
-        if (m_upper_bound < q) {
+        if (m_util.is_numeral(tmp, q) && m_upper_bound < q) {
             m_upper_bound = q;
             if (strict) {
                 m_upper_bound -= get_epsilon(a->get_var());