diff --git a/src/ebmc/ebmc_solver_factory.cpp b/src/ebmc/ebmc_solver_factory.cpp index 9e79dfd42..acd4101e0 100644 --- a/src/ebmc/ebmc_solver_factory.cpp +++ b/src/ebmc/ebmc_solver_factory.cpp @@ -110,16 +110,29 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline) if(smt2_solver.has_value()) { return - [smt2_solver](const namespacet &ns, message_handlert &message_handler) - { - return ebmc_solvert{std::make_unique( - ns, - "ebmc", - "Generated by EBMC " EBMC_VERSION, - "QF_AUFBV", - smt2_solver.value(), - message_handler)}; - }; + [smt2_solver](const namespacet &ns, message_handlert &message_handler) { + if(smt2_solver == smt2_convt::solvert::GENERIC) + { + // --smt2 but no --outfile given. Send to std::cout. + return ebmc_solvert{std::make_unique( + ns, + "ebmc", + "Generated by EBMC " EBMC_VERSION, + "QF_AUFBV", + smt2_solver.value(), + std::cout)}; + } + else + { + return ebmc_solvert{std::make_unique( + ns, + "ebmc", + "Generated by EBMC " EBMC_VERSION, + "QF_AUFBV", + smt2_solver.value(), + message_handler)}; + } + }; } else {