From 7b1cdf60f7c1e962fc68672d5c3da6a1cc12ccf0 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 13 Jul 2026 02:16:40 +0000 Subject: [PATCH] Scope TPTP skolem parameter to solver --- src/cmd_context/tptp_frontend.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 19e42d4c82..65368bfc40 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -9,7 +9,6 @@ #include #include "util/error_codes.h" -#include "util/gparams.h" #include "util/rational.h" #include "util/timeout.h" #include "util/z3_exception.h" @@ -2929,14 +2928,15 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) { register_on_timeout_proc(on_timeout); try { cmd_context ctx; - gparams::set("pi.avoid_skolems", "false"); - ctx.global_params_updated(); tptp_parser p(ctx); p.parse_input(in, current_file ? current_file : "."); p.assert_distinct_objects(); ctx.set_solver_factory(mk_smt_strategic_solver_factory()); + params_ref solver_params; + solver_params.set_bool("pi.avoid_skolems", false); + ctx.get_solver()->updt_params(solver_params); // Optional: dump the parsed goal as an SMT-LIB2 benchmark (env Z3_TPTP_DUMP_SMT2 // gives the output file path). Used to produce SMTLIB versions of TPTP instances.