diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 96a3a6651fe..6d148cfca27 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1135,7 +1135,6 @@ class theory_lra::imp {
 
     void apply_sort_cnstr(enode* n, sort*) {
         TRACE("arith", tout << "sort constraint: " << mk_pp(n->get_owner(), m) << "\n";);
-#if 0
         if (!th.is_attached_to_var(n)) {
             theory_var v = mk_var(n->get_owner(), false);
             lpvar vj = register_theory_var_in_lar_solver(v);
@@ -1148,7 +1147,6 @@ class theory_lra::imp {
                 add_def_constraint(lu_constraints.second);
             }
         }
-#endif
     }
 
     void push_scope_eh() {