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); }