diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index fce725db8..33d09bc8e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1816,6 +1816,7 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); + TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); // increment reference counters diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 659ab6c9f..ef875479f 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -708,7 +708,7 @@ namespace opt { if (fid != m.get_basic_family_id() && fid != pb.get_family_id() && fid != bv.get_family_id() && - !is_uninterp_const(n)) { + (!is_uninterp_const(n) || (!m.is_bool(n) && !bv.is_bv(n)))) { throw found(); } }