diff --git a/vampire.cpp b/vampire.cpp index 65de64868..75198e656 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -562,6 +562,7 @@ void dispatchByMode(Problem* problem) case Options::Mode::CASC: env.options->setIgnoreMissing(Options::IgnoreMissing::WARN); env.options->setSchedule(Options::Schedule::CASC); + env.options->setInputSyntax(Options::InputSyntax::TPTP); env.options->setOutputMode(Options::Output::SZS); env.options->setProof(Options::Proof::TPTP); env.options->setOutputAxiomNames(true); @@ -576,6 +577,7 @@ void dispatchByMode(Problem* problem) case Options::Mode::CASC_HOL: { env.options->setIgnoreMissing(Options::IgnoreMissing::WARN); env.options->setSchedule(Options::Schedule::CASC_HOL_2020); + env.options->setInputSyntax(Options::InputSyntax::TPTP); env.options->setOutputMode(Options::Output::SZS); env.options->setProof(Options::Proof::TPTP); env.options->setOutputAxiomNames(true); @@ -588,6 +590,7 @@ void dispatchByMode(Problem* problem) case Options::Mode::CASC_SAT: env.options->setIgnoreMissing(Options::IgnoreMissing::WARN); env.options->setSchedule(Options::Schedule::CASC_SAT); + env.options->setInputSyntax(Options::InputSyntax::TPTP); env.options->setOutputMode(Options::Output::SZS); env.options->setProof(Options::Proof::TPTP); env.options->setOutputAxiomNames(true);