enable apply_sort_cnstr()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Feb 27, 2020 · 4685317 · 4685317
1 parent 632b185
commit 4685317
Showing 1 changed file with 0 additions and 2 deletions.
diff --git 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() {