From bc75e08a52a71a7479d87b87e970f2afe2f79cb6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 9 Feb 2020 15:48:53 -0800
Subject: [PATCH] fix #2943

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

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 79337f4fe..025ec76d1 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -166,6 +166,8 @@ std::pair<unsigned, int> theory_arith<Ext>::analyze_monomial(expr * m) const {
     int idx          = 0;
     for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
         expr * arg = to_app(m)->get_arg(i);
+        if (m_util.is_numeral(arg))
+            continue;
         if (var == nullptr) {
             var   = arg;
             power = 1;