From d9508926c523f128796b61be5c089f3001b2342f Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 2 Dec 2023 07:43:12 -0800
Subject: [PATCH] ebmc: send output for --smt2 to console when no --outfile is
 given

When no --outfile is given, the option --smt2 now directs the formula to the
console, as opposed to simply dropping it.
---
 src/ebmc/ebmc_solver_factory.cpp | 33 ++++++++++++++++++++++----------
 1 file changed, 23 insertions(+), 10 deletions(-)

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<smt2_dect>(
-        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<smt2_convt>(
+            ns,
+            "ebmc",
+            "Generated by EBMC " EBMC_VERSION,
+            "QF_AUFBV",
+            smt2_solver.value(),
+            std::cout)};
+        }
+        else
+        {
+          return ebmc_solvert{std::make_unique<smt2_dect>(
+            ns,
+            "ebmc",
+            "Generated by EBMC " EBMC_VERSION,
+            "QF_AUFBV",
+            smt2_solver.value(),
+            message_handler)};
+        }
+      };
   }
   else
   {