From d7d687703195a36fe0725278f5c05b6defa0dd2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Apr 2020 06:34:03 -0700 Subject: [PATCH] fix #3958 Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 04bf40b5e..76c25e2c5 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1140,7 +1140,8 @@ namespace datatype { TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";); cd = get_non_rec_constructor_core(ty, forbidden_set); SASSERT(forbidden_set.back() == ty); - SASSERT(cd.first); + if (!cd.first) // datatypes are not completed on parse errors + throw default_exception("constructor not available"); return cd.first; }