diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 1257adea4..21f65dd28 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2306,21 +2306,6 @@ namespace smt {
         }
     }
 
-#if 0
-    /**
-       \brief Return true if it was possible to patch all variables in m_to_patch.
-    */
-    template<typename Ext>
-    bool theory_arith<Ext>::reduce_feasible() {
-        for (theory_vars v : sort_by_coefficients()) {
-            
-        }
-        m_value[v] += delta;
-        if (is_base(v) && !m_to_patch.contains(v) && (below_lower(v) || above_upper(v))) {
-            m_value[v] -= delta;
-        }
-    }
-#endif
 
     /**
        \brief Return true if it was possible to patch all variables in m_to_patch.
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index a588368b3..1eef58ce5 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -500,7 +500,6 @@ class solve_eqs_tactic : public tactic {
 
         bool is_compatible(goal const& g, unsigned idx, vector<nnf_context> const & path, expr* v, expr* eq) {
             expr_mark occ;
-            //std::cout << mk_pp(v, m()) << "\n";
             mark_occurs(occ, g, v);
             return is_goal_compatible(g, occ, idx, v, eq) && is_path_compatible(occ, path, v, eq);
         }