diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 7e143e1a3..12ca136c5 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2254,7 +2254,12 @@ var * ast_manager::mk_var(unsigned idx, sort * s) {
     unsigned sz     = var::get_obj_size();
     void * mem      = allocate_node(sz);
     var * new_node  = new (mem) var(idx, s);
-    return register_node(new_node);
+    var * r         = register_node(new_node);
+
+    if (m_trace_stream && r == new_node) {
+        *m_trace_stream << "[mk-var] #" << r->get_id() << "\n";
+    }
+    return r;
 }
 
 app * ast_manager::mk_label(bool pos, unsigned num_names, symbol const * names, expr * n) {
diff --git a/src/parsers/util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp
index 0d076aadd..df1f6cd00 100644
--- a/src/parsers/util/pattern_validation.cpp
+++ b/src/parsers/util/pattern_validation.cpp
@@ -48,7 +48,7 @@ struct pattern_validation_functor {
 
     bool is_forbidden(func_decl const * decl) {
         family_id fid = decl->get_family_id();
-        if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
+        if (fid == m_bfid && decl->get_decl_kind() != OP_EQ && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
             return true;
         if (fid == m_lfid)
             return true;