diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index 9ce056121..d96667378 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -20,6 +20,7 @@ SRC = \
       live_signal.cpp \
       main.cpp \
       neural_liveness.cpp \
+      output_file.cpp \
       output_verilog.cpp \
       random_traces.cpp \
       ranking_function.cpp \
diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
index a3cc292a4..03a5d4944 100644
--- a/src/ebmc/ebmc_base.cpp
+++ b/src/ebmc/ebmc_base.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/string2int.h>
-#include <util/unicode.h>
 
 #include <solvers/prop/literal_expr.h>
 #include <solvers/sat/satcheck.h>
@@ -29,10 +28,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "ebmc_version.h"
+#include "output_file.h"
 #include "report_results.h"
 
 #include <chrono>
-#include <fstream>
 #include <iostream>
 
 /*******************************************************************\
@@ -277,20 +276,13 @@ int ebmc_baset::do_bit_level_bmc()
   {
     if(cmdline.isset("outfile"))
     {
-      const std::string filename = cmdline.get_value("outfile");
-      std::ofstream out(widen_if_needed(filename));
+      auto outfile = output_filet{cmdline.get_value("outfile")};
 
-      if(!out)
-      {
-        message.error() << "Failed to open `" << filename << "'"
-                        << messaget::eom;
-        return 1;
-      }
-
-      message.status() << "Writing DIMACS CNF to `" << filename << "'"
+      message.status() << "Writing DIMACS CNF to `" << outfile.name() << "'"
                        << messaget::eom;
 
-      dimacs_cnf_writert dimacs_cnf_writer{out, message.get_message_handler()};
+      dimacs_cnf_writert dimacs_cnf_writer{
+        outfile.stream(), message.get_message_handler()};
 
       return do_bit_level_bmc(dimacs_cnf_writer, true);
     }
diff --git a/src/ebmc/ebmc_error.h b/src/ebmc/ebmc_error.h
index 947dbddff..f8d04a018 100644
--- a/src/ebmc/ebmc_error.h
+++ b/src/ebmc/ebmc_error.h
@@ -9,8 +9,9 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef EBMC_ERROR_H
 #define EBMC_ERROR_H
 
+#include <util/source_location.h>
+
 #include <sstream>
-#include <string>
 
 class ebmc_errort
 {
diff --git a/src/ebmc/ebmc_solvers.cpp b/src/ebmc/ebmc_solvers.cpp
deleted file mode 100644
index a524ae2a6..000000000
--- a/src/ebmc/ebmc_solvers.cpp
+++ /dev/null
@@ -1,68 +0,0 @@
-/*******************************************************************\
-
-Module: EBMC's Solvers
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include <util/cmdline.h>
-#include <util/unicode.h>
-
-#include <solvers/flattening/boolbv.h>
-#include <solvers/sat/dimacs_cnf.h>
-#include <solvers/sat/satcheck.h>
-#include <solvers/smt2/smt2_dec.h>
-
-#include <fstream>
-#include <iostream>
-
-#ifdef HAVE_PROVER
-#include <prover/prover_sat.h>
-#include <prover/lifter.h>
-#endif
-
-#include "dimacs_writer.h"
-#include "ebmc_base.h"
-#include "ebmc_solver_factory.h"
-#include "ebmc_version.h"
-#include "show_formula_solver.h"
-
-/*******************************************************************\
-
-Function: ebmc_baset::do_bit_level_bmc
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int ebmc_baset::do_bit_level_bmc()
-{
-  if(cmdline.isset("outfile"))
-  {
-    const std::string filename=cmdline.get_value("outfile");
-    std::ofstream out(widen_if_needed(filename));
-
-    if(!out)
-    {
-      message.error() << "Failed to open `" << filename << "'" << messaget::eom;
-      return 1;
-    }
-
-    dimacs_cnf_writert dimacs_cnf_writer{out, message.get_message_handler()};
-
-    return do_bit_level_bmc(dimacs_cnf_writer, true);
-  }
-  else
-  {
-    satcheckt satcheck{message.get_message_handler()};
-
-    message.status() << "Using " << satcheck.solver_text() << messaget::eom;
-
-    return do_bit_level_bmc(satcheck, false);
-  }
-}
diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp
index d72bc2e2b..5c2856f09 100644
--- a/src/ebmc/neural_liveness.cpp
+++ b/src/ebmc/neural_liveness.cpp
@@ -13,7 +13,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/string2int.h>
 #include <util/tempdir.h>
 #include <util/tempfile.h>
-#include <util/unicode.h>
 
 #include <temporal-logic/temporal_expr.h>
 #include <verilog/sva_expr.h>
@@ -21,6 +20,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "live_signal.h"
+#include "output_file.h"
 #include "random_traces.h"
 #include "ranking_function.h"
 #include "report_results.h"
@@ -199,13 +199,10 @@ neural_livenesst::dump_vcd_files(temp_dirt &temp_dir)
     [&, trace_nr = 0ull, outfile_prefix](trans_tracet trace) mutable -> void {
       namespacet ns(transition_system.symbol_table);
       auto filename = outfile_prefix + std::to_string(trace_nr + 1);
-      std::ofstream out(widen_if_needed(filename));
-
-      if(!out)
-        throw ebmc_errort() << "failed to write trace to " << filename;
-
-      message.progress() << "*** Writing " << filename << messaget::eom;
-      show_trans_trace_vcd(trace, message, ns, out);
+      auto outfile = output_filet{filename};
+      message.progress() << "*** Writing to " << outfile.name()
+                         << messaget::eom;
+      show_trans_trace_vcd(trace, message, ns, outfile.stream());
     };
 }
 
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
index ac546de19..67c17bdd4 100644
--- a/src/ebmc/random_traces.cpp
+++ b/src/ebmc/random_traces.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "output_file.h"
 #include "waveform.h"
 
 #include <algorithm>
@@ -182,15 +183,12 @@ int random_traces(const cmdlinet &cmdline, message_handlert &message_handler)
     {
       PRECONDITION(outfile_prefix.has_value());
       auto filename = outfile_prefix.value() + std::to_string(trace_nr + 1);
-      std::ofstream out(widen_if_needed(filename));
+      auto outfile = output_filet{filename};
 
-      if(!out)
-        throw ebmc_errort() << "failed to write trace to " << filename;
-
-      consolet::out() << "*** Writing " << filename << '\n';
+      consolet::out() << "*** Writing " << outfile.name() << '\n';
 
       messaget message(message_handler);
-      show_trans_trace_vcd(trace, message, ns, out);
+      show_trans_trace_vcd(trace, message, ns, outfile.stream());
     }
     else if(cmdline.isset("waveform"))
     {
@@ -294,23 +292,13 @@ int random_trace(const cmdlinet &cmdline, message_handlert &message_handler)
     else if(cmdline.isset("vcd"))
     {
       auto filename = cmdline.get_value("vcd");
-      messaget message(message_handler);
-
-      if(filename == "-")
-      {
-        show_trans_trace_vcd(trace, message, ns, std::cout);
-      }
-      else
-      {
-        std::ofstream out(widen_if_needed(filename));
-
-        if(!out)
-          throw ebmc_errort() << "failed to write trace to " << filename;
+      auto outfile = output_filet{filename};
 
+      if(filename != "-")
         consolet::out() << "*** Writing " << filename << '\n';
 
-        show_trans_trace_vcd(trace, message, ns, out);
-      }
+      messaget message(message_handler);
+      show_trans_trace_vcd(trace, message, ns, outfile.stream());
     }
     else // default
     {
@@ -352,13 +340,9 @@ void random_traces(
   auto consumer = [&, trace_nr = 0ull](trans_tracet trace) mutable -> void {
     namespacet ns(transition_system.symbol_table);
     auto filename = outfile_prefix + std::to_string(trace_nr + 1);
-    std::ofstream out(widen_if_needed(filename));
-
-    if(!out)
-      throw ebmc_errort() << "failed to write trace to " << filename;
-
+    auto outfile = output_filet{filename};
     messaget message(message_handler);
-    show_trans_trace_vcd(trace, message, ns, out);
+    show_trans_trace_vcd(trace, message, ns, outfile.stream());
 
     trace_nr++;
   };
diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
index 07c989e7b..2f45f347b 100644
--- a/src/ebmc/report_results.cpp
+++ b/src/ebmc/report_results.cpp
@@ -12,13 +12,12 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "report_results.h"
 
 #include <util/json.h>
-#include <util/unicode.h>
 #include <util/xml.h>
 
 #include "ebmc_error.h"
+#include "output_file.h"
 #include "waveform.h"
 
-#include <fstream>
 #include <iostream>
 
 /*******************************************************************\
@@ -42,9 +41,7 @@ void report_results(
   if(cmdline.isset("json-result"))
   {
     auto filename = cmdline.get_value("json-result");
-    std::ofstream out(widen_if_needed(filename));
-    if(!out)
-      throw ebmc_errort() << "failed to open " << filename;
+    auto outfile = output_filet{filename};
 
     json_objectt json_results;
     auto &json_properties = json_results["properties"].make_array();
@@ -65,7 +62,7 @@ void report_results(
       json_properties.push_back(std::move(json_property));
     }
 
-    out << json_results;
+    outfile.stream() << json_results;
   }
 
   if(
@@ -167,10 +164,11 @@ void report_results(
       if(property.has_witness_trace())
       {
         std::string vcdfile = cmdline.get_value("vcd");
-        std::ofstream vcd(widen_if_needed(vcdfile));
+        auto outfile = output_filet{vcdfile};
 
         messaget message(message_handler);
-        show_trans_trace_vcd(property.witness_trace.value(), message, ns, vcd);
+        show_trans_trace_vcd(
+          property.witness_trace.value(), message, ns, outfile.stream());
 
         break;
       }
diff --git a/src/ebmc/show_properties.cpp b/src/ebmc/show_properties.cpp
index 58b9b7692..aa84ab612 100644
--- a/src/ebmc/show_properties.cpp
+++ b/src/ebmc/show_properties.cpp
@@ -8,12 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/json.h>
 #include <util/json_irep.h>
-#include <util/unicode.h>
 #include <util/xml.h>
 #include <util/xml_irep.h>
 
 #include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "output_file.h"
 
 #include <iostream>
 
@@ -97,16 +97,6 @@ void ebmc_baset::json_properties(const std::string &file_name)
     json.push_back(std::move(json_property));
   }
 
-  if(file_name == "-")
-  {
-    std::cout << json;
-  }
-  else
-  {
-    std::ofstream out(widen_if_needed(file_name));
-    if(!out)
-      throw ebmc_errort() << "failed to open " << file_name;
-
-    out << json;
-  }
+  auto outfile = output_filet{file_name};
+  outfile.stream() << json;
 }
diff --git a/src/ebmc/show_trans.cpp b/src/ebmc/show_trans.cpp
index 8de6b587a..0c1a2bbc3 100644
--- a/src/ebmc/show_trans.cpp
+++ b/src/ebmc/show_trans.cpp
@@ -8,15 +8,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "show_trans.h"
 
-#include <util/unicode.h>
-
 #include <verilog/expr2verilog.h>
 
 #include "ebmc_base.h"
 #include "ebmc_version.h"
+#include "output_file.h"
 #include "output_verilog.h"
 
-#include <fstream>
 #include <iostream>
 
 /*******************************************************************\
@@ -268,17 +266,8 @@ int show_transt::show_trans_verilog_rtl()
   if(cmdline.isset("outfile"))
   {
     const std::string filename=cmdline.get_value("outfile");
-    std::ofstream out(widen_if_needed(filename));
-
-    if(!out)
-    {
-      std::cerr << "Failed to open `"
-                << filename
-                << "'" << '\n';
-      return 1;
-    }
-
-    show_trans_verilog_rtl(out);
+    auto outfile = output_filet{filename};
+    show_trans_verilog_rtl(outfile.stream());
   }
   else
     show_trans_verilog_rtl(std::cout);
@@ -306,17 +295,8 @@ int show_transt::show_trans_verilog_netlist()
   if(cmdline.isset("outfile"))
   {
     const std::string filename=cmdline.get_value("outfile");
-    std::ofstream out(widen_if_needed(filename));
-
-    if(!out)
-    {
-      std::cerr << "Failed to open `"
-                << filename
-                << "'" << '\n';
-      return 1;
-    }
-
-    show_trans_verilog_netlist(out);
+    auto outfile = output_filet{filename};
+    show_trans_verilog_netlist(outfile.stream());
   }
   else
     show_trans_verilog_netlist(std::cout);
diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp
index dcbf8d54b..cc9017ba0 100644
--- a/src/ebmc/transition_system.cpp
+++ b/src/ebmc/transition_system.cpp
@@ -25,6 +25,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "ebmc_error.h"
 #include "ebmc_version.h"
+#include "output_file.h"
 
 #include <fstream>
 #include <iostream>
@@ -273,10 +274,8 @@ int get_transition_system(
   if(cmdline.isset("modules-xml"))
   {
     auto filename = cmdline.get_value("modules-xml");
-    std::ofstream out(widen_if_needed(filename));
-    if(!out)
-      throw ebmc_errort() << "failed to open " << filename;
-    show_modules_xml(transition_system.symbol_table, out);
+    auto outfile = output_filet{filename};
+    show_modules_xml(transition_system.symbol_table, outfile.stream());
     return 0;
   }