fix #3958

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 14, 2020 · d7d6877 · d7d6877
1 parent 387964f
commit d7d6877
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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;
     }