diff --git a/src/solvers/sat/dimacs_cnf.cpp b/src/solvers/sat/dimacs_cnf.cpp
index 63d333d24b9..2206603e28d 100644
--- a/src/solvers/sat/dimacs_cnf.cpp
+++ b/src/solvers/sat/dimacs_cnf.cpp
@@ -9,7 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "dimacs_cnf.h"
 
+#include <util/magic.h>
+
 #include <iostream>
+#include <sstream>
 
 dimacs_cnft::dimacs_cnft():break_lines(false)
 {
@@ -60,9 +63,23 @@ static void write_dimacs_clause(
 
 void dimacs_cnft::write_clauses(std::ostream &out)
 {
+  std::size_t count = 0;
+  std::stringstream output_block;
   for(clausest::const_iterator it=clauses.begin();
       it!=clauses.end(); it++)
-    write_dimacs_clause(*it, out, break_lines);
+  {
+    write_dimacs_clause(*it, output_block, break_lines);
+
+    // print the block once in a while
+    if(++count % CNF_DUMP_BLOCK_SIZE == 0)
+    {
+      out << output_block.str();
+      output_block.str("");
+    }
+  }
+
+  // make sure the final block is printed as well
+  out << output_block.str();
 }
 
 void dimacs_cnf_dumpt::lcnf(const bvt &bv)
diff --git a/src/util/magic.h b/src/util/magic.h
index e3bfbdeeae3..48c72436e2d 100644
--- a/src/util/magic.h
+++ b/src/util/magic.h
@@ -7,6 +7,7 @@
 
 #include <cstddef>
 
+const std::size_t CNF_DUMP_BLOCK_SIZE = 4096;
 const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000;
 const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16;