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.