From 4518f4fe02dcad10a88e7020262cf660563881a9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Sep 2022 20:31:55 -0700
Subject: [PATCH] fix #6352

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 535500cae..041d6740a 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -904,18 +904,16 @@ namespace datatype {
     bool util::is_well_founded(unsigned num_types, sort* const* sorts) {
         buffer<bool> well_founded(num_types, false);
         obj_map<sort, unsigned> sort2id;
-        for (unsigned i = 0; i < num_types; ++i) {
+        for (unsigned i = 0; i < num_types; ++i) 
             sort2id.insert(sorts[i], i);
-        }
         unsigned num_well_founded = 0, id = 0;
         bool changed;
         ptr_vector<sort> subsorts;
         do {
             changed = false;
             for (unsigned tid = 0; tid < num_types; tid++) {
-                if (well_founded[tid]) {
+                if (well_founded[tid]) 
                     continue;
-                }
                 sort* s = sorts[tid];
                 def const& d = get_def(s);
                 for (constructor const* c : d) {
@@ -923,9 +921,12 @@ namespace datatype {
                         subsorts.reset();
                         get_subsorts(a->range(), subsorts);
                         for (sort* srt : subsorts) {
-                            if (sort2id.find(srt, id) && !well_founded[id]) {
-                                goto next_constructor;
+                            if (sort2id.find(srt, id)) {
+                                if (!well_founded[id]) 
+                                    goto next_constructor;
                             }
+                            else if (is_datatype(srt))
+                                break;
                         }
                     }
                     changed = true;