diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 6e739a499..8995f7fba 100644
--- 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
index 77b3f14d5..1c899ef18 100644
--- 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";);