diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 4f9a88490..5c0abf6b8 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1726,8 +1726,6 @@ ast * ast_manager::register_node_core(ast * n) {
     }
 
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
-    static unsigned s_counter = 0;
-
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h
index 35545e975..4831280af 100644
--- a/src/math/automata/symbolic_automata.h
+++ b/src/math/automata/symbolic_automata.h
@@ -130,13 +130,13 @@ private:
         else {
             //true case
             curr_bv.push_back(true);
-            ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);			
+            ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
             generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
             curr_bv.pop_back();
             
             //false case
             curr_bv.push_back(false);
-			ref_t neg(m_ba.mk_not(constraints[i]), m);
+            ref_t neg(m_ba.mk_not(constraints[i]), m);
             ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
             generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
             curr_bv.pop_back();