From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 18 Oct 2014 21:56:21 +0000 (+0200)
Subject: Fix assertion.
X-Git-Tag: cvc5-1.0.0~6551
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0c6239f4e6e2e7756922764a4d7bb990043c29f;p=cvc5.git

Fix assertion.
---

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 8214f23e2..c8ce9833c 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -320,7 +320,7 @@ public:
     return false;
   }
   static bool isNullaryApplyConstructor( Node n ){
-    Assert( n.getKind()==APPLY_CONSTRUCTOR );
+    Assert( n.getKind()==kind::APPLY_CONSTRUCTOR );
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( n[i].getType().isDatatype() ){
         return false;