From 908254752b851ccbf6bf31e51171b8e078378ebb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 9 Oct 2019 15:28:28 -0700
Subject: [PATCH] simplify

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

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index b655f7582..d1434af31 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1232,15 +1232,10 @@ namespace smt {
             else if (ctx.e_internalized(m)) {
                 ADD_OCC(m);
             }
-            else if (!ctx.e_internalized(m)) {
+            else {
                 ctx.internalize(m, false);
                 ADD_OCC(m);
             }
-            else {
-                TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
-                UNREACHABLE();
-                return;
-            }
         }
 
         // Update the number of occurrences in the result vector.