#5752

Z3Prover · Jan 6, 2022 · 592b1d7 · 592b1d7
1 parent d14f00d
commit 592b1d7
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
@@ -158,7 +158,6 @@ namespace smt {
 
         void mark_as_interpreted() {
             SASSERT(!m_interpreted);
-            SASSERT(m_owner->get_num_args() == 0);
             SASSERT(m_class_size == 1);
             m_interpreted = true;
         }

diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
@@ -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);
         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();
         TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
         TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);