fix #7264

NikolajBjorner · NikolajBjorner · commit 8e482df62a59 · 2024-06-21T08:37:23.000-07:00
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())

Original file line number	Diff line number	Diff line change
`@@ -481,6 +481,10 @@ struct evaluator_cfg : public default_rewriter_cfg {`
`481`	`481`	`return BR_DONE;`
`482`	`482`	`}`
`483`	`483`	`}`
	`484`	`+ else if (m_dt.is_constructor(f)) {`
	`485`	`+ result = m.mk_app(f, num, args);`
	`486`	`+ return BR_DONE;`
	`487`	`+ }`
`484`	`488`
`485`	`489`	`if (fi) {`
`486`	`490`	`if (fi->is_partial())`