From 208cc56861fbba7a5466e780a6c5d7630ce43f46 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Jul 2026 12:51:52 -0700
Subject: [PATCH] fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/elim_unconstrained.cpp |  2 ++
 src/cmd_context/tptp_frontend.cpp          | 24 ++++++++--------------
 src/tactic/core/elim_uncnstr_tactic.cpp    |  2 +-
 3 files changed, 11 insertions(+), 17 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 76a622a456..120fe06729 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -425,6 +425,8 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
 void elim_unconstrained::reduce() {
     if (!m_config.m_enabled)
         return;
+    if (m.has_type_vars())
+        return;
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
     m_inverter.set_model_converter(mc.get());
     m_created_compound = true;
diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index b4a1189000..57ab4c3fc0 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -8,20 +8,21 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#include "util/error_codes.h"
+#include "util/rational.h"
+#include "util/timeout.h"
+#include "util/z3_exception.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/expr_abstract.h"
 #include "ast/ast_util.h"
 #include "ast/polymorphism_util.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include "solver/solver.h"
 #include "cmd_context/cmd_context.h"
 #include "cmd_context/tptp_frontend.h"
-#include "smt/smt_solver.h"
-#include "solver/solver.h"
-#include "util/error_codes.h"
-#include "util/rational.h"
-#include "util/timeout.h"
-#include "util/z3_exception.h"
+
+
 
 bool g_display_statistics = false;
 bool g_display_model = false;
@@ -2796,16 +2797,7 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
         p.parse_input(in, current_file ? current_file : ".");
         p.assert_distinct_objects();
 
-        // Polymorphic (TF1/TH1) problems are instantiated on demand by
-        // theory_polymorphism inside the smt core. The strategic solver's tactic
-        // preprocessing (e.g. unconstrained-subterm elimination) runs before the
-        // core and can discard a monomorphic instance that only occurs in the
-        // conjecture, severing it from its polymorphic axiom. Use the plain smt
-        // solver in that case so instantiation is not defeated by preprocessing.
-        if (ctx.m().has_type_vars())
-            ctx.set_solver_factory(mk_smt_solver_factory());
-        else
-            ctx.set_solver_factory(mk_smt_strategic_solver_factory());
+        ctx.set_solver_factory(mk_smt_strategic_solver_factory());
 
         // Suppress default check-sat output; TPTP frontend reports SZS status explicitly.
         std::ostringstream sink;
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 6807cdaa1e..a0eaeead94 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -945,7 +945,7 @@ class elim_uncnstr_tactic : public tactic {
         collect_occs p;
         p(*g, m_vars);
         disable_quantified(g);
-        if (m_vars.empty() || recfun::util(m()).has_rec_defs()) {
+        if (m_vars.empty() || recfun::util(m()).has_rec_defs() || m().has_type_vars()) {
             result.push_back(g.get());
             // did not increase depth since it didn't do anything.
             return;