From 8e482df62a59520499e575e21b9e01bd889ddddb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 21 Jun 2024 08:37:23 -0700
Subject: [PATCH] fix #7264

---
 src/model/model_evaluator.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 6f218934b..2446609c6 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -481,6 +481,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 return BR_DONE;
             }
         }
+        else if (m_dt.is_constructor(f)) {
+            result = m.mk_app(f, num, args);
+            return BR_DONE;
+        }
 
         if (fi) {
             if (fi->is_partial())