diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 373838c15..f636c726b 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -461,7 +461,6 @@ namespace sat {
     }
 
     void solver::dettach_clause(clause & c) {
-        TRACE("sat", tout << c.id() << "\n";);
         if (c.size() == 3)
             dettach_ter_clause(c);
         else
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index bff421d12..4291590c6 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -618,10 +618,8 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::remove_fixed_vars_from_base() {
         int num = get_num_vars();
-        //std::cout << "num vars " << num << "\n";
         for (theory_var v = 0; v < num; v++) {
             if (is_base(v) && is_fixed(v)) {
-                //std::cout << "fixed base " << v << " \n"; // << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";
                 row const & r = m_rows[get_var_row(v)];
                 typename vector<row_entry>::const_iterator it  = r.begin_entries();
                 typename vector<row_entry>::const_iterator end = r.end_entries();