Add nullary operator metakind.

1 files changed, 3 insertions, 6 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 31721b2ef..6d98b940b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -464,12 +464,6 @@ public:
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::VARIABLE;
   }
-  inline bool isUninterpretedVar() const {
-    assertTNodeNotExpired();
-    return getMetaKind() == kind::metakind::VARIABLE &&
-           getKind() != kind::UNIVERSE_SET && 
-           getKind() != kind::SEP_NIL;
-  }
 
   inline bool isClosure() const {
     assertTNodeNotExpired();
@@ -1259,6 +1253,9 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
   case kind::metakind::CONSTANT:
     IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind");
 
+  case kind::metakind::NULLARY_OPERATOR:
+    IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind");
+
   default:
     Unhandled(mk);
   }