diff --git a/CHANGELOG b/CHANGELOG
index 8608e7dc6..fd6f4ab57 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -8,6 +8,7 @@
 * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
 * SystemVerilog: set membership operator
 * SystemVerilog: named sequences
+* ebmc: --smt-netlist and --dot-netlist now honor --outfile
 
 # EBMC 5.3
 
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index f2a30ceca..5f673cfe8 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ic3_engine.h"
 #include "liveness_to_safety.h"
 #include "neural_liveness.h"
+#include "output_file.h"
 #include "property_checker.h"
 #include "random_traces.h"
 #include "ranking_function.h"
@@ -274,9 +275,12 @@ int ebmc_parse_optionst::doit()
         netlistt netlist;
         if(ebmc_base.make_netlist(netlist))
           return 1;
-        std::cout << "digraph netlist {\n";
-        netlist.output_dot(std::cout);
-        std::cout << "}\n";
+        auto filename =
+          cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
+        output_filet outfile{filename};
+        outfile.stream() << "digraph netlist {\n";
+        netlist.output_dot(outfile.stream());
+        outfile.stream() << "}\n";
         return 0;
       }
 
@@ -285,11 +289,15 @@ int ebmc_parse_optionst::doit()
         netlistt netlist;
         if(ebmc_base.make_netlist(netlist))
           return 1;
-        std::cout << "-- Generated by EBMC " << EBMC_VERSION << '\n';
-        std::cout << "-- Generated from "
-                  << ebmc_base.transition_system.main_symbol->name << '\n';
-        std::cout << '\n';
-        netlist.output_smv(std::cout);
+        auto filename =
+          cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
+        output_filet outfile{filename};
+        outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
+        outfile.stream() << "-- Generated from "
+                         << ebmc_base.transition_system.main_symbol->name
+                         << '\n';
+        outfile.stream() << '\n';
+        netlist.output_smv(outfile.stream());
         return 0;
       }