fix #7102

Z3Prover · Jan 28, 2024 · f8a3b6f · f8a3b6f
1 parent 2af1cff
commit f8a3b6f
Showing 1 changed file with 20 additions and 1 deletion.
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
 #include "ast/recfun_decl_plugin.h"
+#include "ast/polymorphism_util.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/arith_rewriter.h"
@@ -371,7 +372,20 @@ struct evaluator_cfg : public default_rewriter_cfg {
     bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) {
         func_interp * fi = m_model.get_func_interp(f);
         def = nullptr;
-        if (fi != nullptr) {
+        if (fi) {
+            if (fi->is_partial()) {
+                if (m_model_completion) {
+                    sort * s   = f->get_range();
+                    expr * val = m_model.get_some_value(s);
+                    fi->set_else(val);
+                }
+                else
+                    return false;
+            }
+            def = fi->get_interp();
+            SASSERT(def != nullptr);
+        }
+        else if (f->is_polymorphic() && (fi = m_model.get_func_interp(m.poly_root(f)))) {
             if (fi->is_partial()) {
                 if (m_model_completion) {
                     sort * s   = f->get_range();
@@ -382,7 +396,12 @@ struct evaluator_cfg : public default_rewriter_cfg {
                     return false;
             }
             def = fi->get_interp();
+            polymorphism::substitution subst(m);
+            polymorphism::util util(m);
+            util.unify(f, m.poly_root(f), subst);
+            def = subst(def);
             SASSERT(def != nullptr);
+
         }
         else if (m_model_completion &&
             (f->get_family_id() == null_family_id ||