From 16d4e2f5d1b2de3ee5fc62e20afeb5678b66a314 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 29 Jun 2018 16:10:15 -0700
Subject: [PATCH] regression fix

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 513248d4b..dda853760 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -862,9 +862,6 @@ public:
         if (ctx().e_internalized(term) && th.is_attached_to_var(ctx().get_enode(term))) {
             // skip
         }
-        else if (a.is_numeral(term)) {
-            mk_enode(term);
-        }
         else {
             internalize_def(term);
         }