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.
diffblue · Dec 2, 2023 · d950892 · d950892
1 parent e429921
commit d950892
Showing 1 changed file with 23 additions and 10 deletions.
diff --git 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
   {