mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Set TPTP pi.avoid_skolems globally

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 02:15:08 +00:00 • committed by GitHub
parent 0000e16851
commit d4e177c95e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/tptp_frontend.cpp
View file

@ -9,6 +9,7 @@
#include <unordered_set>
#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 : ".");