From d4e177c95e0bc99daa4ab6e5aa5a49345a743725 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 13 Jul 2026 02:15:08 +0000 Subject: [PATCH] Set TPTP pi.avoid_skolems globally --- src/cmd_context/tptp_frontend.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index e452651571..19e42d4c82 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -9,6 +9,7 @@ #include #include "util/error_codes.h" +#include "util/gparams.h" #include "util/rational.h" #include "util/timeout.h" #include "util/z3_exception.h" @@ -2928,6 +2929,8 @@ 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 : ".");