From 081001971deb57b9e9ce299b704e920ecd9279d4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Dec 2019 01:45:46 -0800
Subject: [PATCH] fix #2794

---
 src/ast/datatype_decl_plugin.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 1e6881bee..9be1b79c2 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -1213,6 +1213,7 @@ namespace datatype {
     }
 
     unsigned util::get_datatype_num_constructors(sort * ty) {
+		if (!is_declared(ty)) return 0;
         def const& d = get_def(ty->get_name());
         return d.constructors().size();
     }