From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 17:12:18 +0000 (+0000)
Subject: fix to TNode assertion (which is too strict, given lax ordering requirements on stati... 
X-Git-Tag: cvc5-1.0.0~7488
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=251841986bb6a68d18350ed76135507b63ef29b6;p=cvc5.git

fix to TNode assertion (which is too strict, given lax ordering requirements on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others
---

diff --git a/src/expr/node.h b/src/expr/node.h
index a3b8853a0..42e9f4253 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1022,7 +1022,8 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
   if(ref_count) {
     d_nv->inc();
   } else {
-    Assert(d_nv->d_rc > 0, "TNode constructed from NodeValue with rc == 0");
+    Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::s_null,
+           "TNode constructed from NodeValue with rc == 0");
   }
 }