diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 8646a0f20..65f1390d0 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -727,7 +727,7 @@ public: m_sorts.emplace("$real", m_arith.mk_real()); } - void parse_stream(std::istream& in, std::string const& current_file) { + void parse_input(std::istream& in, std::string const& current_file) { std::ostringstream buf; buf << in.rdbuf(); m_input = buf.str(); @@ -744,11 +744,11 @@ public: out << "failed to open file '" << filename << "'"; throw parse_error(out.str()); } - parse_stream(in, filename); + parse_input(in, filename); } void parse_stream(std::istream& in) { - parse_stream(in, "."); + parse_input(in, "."); } bool has_conjecture() const { return m_has_conjecture; } @@ -792,7 +792,7 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) { ctx.set_solver_factory(mk_smt_strategic_solver_factory()); tptp_parser p(ctx); - p.parse_stream(in, current_file ? current_file : "."); + p.parse_input(in, current_file ? current_file : "."); // Suppress default check-sat output; TPTP frontend reports SZS status explicitly. std::ostringstream sink; diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp index b40be4d91..44949656c 100644 --- a/src/test/tptp.cpp +++ b/src/test/tptp.cpp @@ -54,8 +54,6 @@ R"(fof(a1,axiom, p(a)).)", }; for (auto const& c : cases) { std::string out = run_tptp(c.input); - if (out.find(c.expected_status) == std::string::npos) - std::cerr << "Unexpected TPTP status for case: " << c.name << "\n" << out << "\n"; ENSURE(out.find(c.expected_status) != std::string::npos); } }