From 0b8335e7768f30a6a941372dc159ce7e1b8b4c07 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Jul 2026 19:21:25 -0700 Subject: [PATCH] Set `pi.avoid_skolems=false` for TPTP solver runs (#10100) The TPTP frontend was not forcing `pi.avoid_skolems=false`, so TPTP problems could be solved with the default pattern-inference behavior instead of the intended frontend-specific setting. This change applies the override directly to the solver used by TPTP runs. - **What changed** - After constructing the TPTP solver, the frontend now sets `pi.avoid_skolems=false` via solver parameters before `check_sat`. - The override is scoped to the TPTP solver instance instead of mutating process-global parameter state. - **Why this shape** - Keeps the TPTP behavior explicit at the point where the solver is created. - Avoids leaking the parameter change into unrelated solver contexts. - **Code sketch** ```c++ 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); ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- 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..65368bfc40 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -2934,6 +2934,9 @@ static unsigned read_tptp_stream(std::istream& in, char const* 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.