fix #7264

Z3Prover · Jun 21, 2024 · 8e482df · 8e482df
1 parent c137ef7
commit 8e482df
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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())