mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
4c09b7d792
commit
ebc9b7fb4e
|
@ -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
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue