mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 17:38:45 +00:00
Code Activity

#5752

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-06 13:32:50 -08:00
parent d14f00d61a
commit 592b1d7f65
2 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_enode.h
View file

@ -158,7 +158,6 @@ namespace smt {
void mark_as_interpreted() { void mark_as_interpreted() {
SASSERT(!m_interpreted); SASSERT(!m_interpreted);
SASSERT(m_owner->get_num_args() == 0);
SASSERT(m_class_size == 1); SASSERT(m_class_size == 1);
m_interpreted = true; m_interpreted = true;
} }

2
src/smt/smt_internalizer.cpp
View file

@ -974,7 +974,7 @@ namespace smt {
} }
enode * e = enode::mk(m, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true); enode * e = enode::mk(m, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";); TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
if (n->get_num_args() == 0 && m.is_unique_value(n)) if (m.is_unique_value(n))
e->mark_as_interpreted(); e->mark_as_interpreted();
TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";); TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";); TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);