From 47cdb5f46e5df3f22352ed003355612e84d56bf4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 3 Feb 2020 09:14:23 -0800
Subject: [PATCH] fix #2913

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

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 8c744581b..fc5441721 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1225,24 +1225,19 @@ bool theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
 
     for (auto const& ce : p) {
         expr * m = ce.second;
-        if (is_pure_monomial(m)) {
+        if (m_util.is_numeral(m)) {
+            continue;
+        }
+        else if (ctx.e_internalized(m) && !is_pure_monomial(m)) {
+            ADD_OCC(m);
+        }
+        else {
             unsigned num_vars = get_num_vars_in_monomial(m);
             for (unsigned i = 0; i < num_vars; i++) {
                 var_power_pair p = get_var_and_degree(m, i);
                 ADD_OCC(p.first);
             }
         }
-        else if (m_util.is_numeral(m)) {
-            continue;
-        }
-        else if (ctx.e_internalized(m)) {
-            ADD_OCC(m);
-        }
-        else {
-            TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
-            UNREACHABLE();
-            return false;
-        }
     }
 
     // Update the number of occurrences in the result vector.