From a0c6239f4e6e2e7756922764a4d7bb990043c29f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 18 Oct 2014 23:56:21 +0200
Subject: [PATCH] Fix assertion.

---
 src/theory/datatypes/datatypes_rewriter.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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;
-- 
2.30.2