1 files changed, 8 insertions, 1 deletions
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index decd57045..6df7ad76f 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -34,13 +34,17 @@ namespace expr {
  * This is an ExprValue.
  */
 class ExprValue {
+
+  /** A convenient null-valued expression value */
+  static ExprValue s_null;
+
   /** Maximum reference count possible.  Used for sticky
    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
   static const unsigned MAX_RC = 255;
 
   // this header fits into one 64-bit word
 
-  /** The ID */
+  /** The ID (0 is reserved for the null value) */
   unsigned d_id        : 32;
 
   /** The expression's reference count.  @see cvc4::Expr. */
@@ -65,6 +69,9 @@ class ExprValue {
 
   static size_t next_id;
 
+  /** Private default constructor for the null value. */
+  ExprValue();
+
 public:
   /** Hash this expression.
    *  @return the hash value of this expression. */