diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 8422006677..840c86730e 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -404,7 +404,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
             polymorphism::substitution subst(m);
             polymorphism::util util(m);
             util.unify(f, m.poly_root(f), subst);
-            def = subst(def);
+            expr_ref d = subst(def);
+            m_pinned.push_back(d);
+            def = d;
             SASSERT(def != nullptr);
             
         }
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 64dc77eb59..255254fe41 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -222,7 +222,8 @@ namespace smt {
                 expr * sk_term = m_model_finder.get_inv(q, i, sk_value, *cex, sk_term_gen);
                 if (sk_term != nullptr) {
                     TRACE(model_checker, tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);
-                    SASSERT(!m.is_model_value(sk_term));
+                    // get_inv may return a model value in polymorphic settings;
+                    // this is handled downstream by get_type_compatible_term.
                     max_generation = std::max(sk_term_gen, max_generation);
                     sk_value = sk_term;
                 }
diff --git a/src/smt/theory_polymorphism.h b/src/smt/theory_polymorphism.h
index 613c1a8dd5..95e0afc136 100644
--- a/src/smt/theory_polymorphism.h
+++ b/src/smt/theory_polymorphism.h
@@ -67,8 +67,18 @@ namespace smt {
         }
 
         final_check_status final_check_eh(unsigned) override {
-            if (m_inst.pending()) 
+            if (m_inst.pending()) {
+                // There are still polymorphic axioms to instantiate. Force the
+                // solver to fail under the theory assumption so that a new
+                // research round (see should_research) can assert the new
+                // instances. Assigning the negation of the (already true)
+                // assumption creates a conflict, so we must return FC_CONTINUE
+                // to let conflict resolution turn it into l_false; returning
+                // FC_DONE here would report l_true while the context is
+                // inconsistent, violating a core search invariant.
                 ctx.assign(~mk_literal(m_assumption), nullptr);
+                return FC_CONTINUE;
+            }
             return FC_DONE;
         }