diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 00b6260fc..1ceff2391 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2005,11 +2005,6 @@ public:
     }
 
     bool can_propagate() {
-#if 0
-        if (ctx().at_base_level() && has_delayed_constraints()) {
-            // we could add the delayed constraints here directly to the tableau instead of using bounds variables.
-        }
-#endif
         return m_asserted_atoms.size() > m_asserted_qhead;
     }
 
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index bca13366f..c26e7b9eb 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -93,6 +93,7 @@ class elim_uncnstr_tactic : public tactic {
             }
             
             v = m().mk_fresh_const(nullptr, m().get_sort(t));
+            std::cout << mk_pp(t, m()) << " -> " << mk_pp(v, m()) << "\n";
             TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";);
             TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";);
             m_fresh_vars.push_back(v);