diff --git a/src/solvers/flattening/bv_dimacs.cpp b/src/solvers/flattening/bv_dimacs.cpp
index ddb8c19f27c..9af80fabfeb 100644
--- a/src/solvers/flattening/bv_dimacs.cpp
+++ b/src/solvers/flattening/bv_dimacs.cpp
@@ -16,6 +16,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream> // IWYU pragma: keep
 #include <iostream>
 
+bv_dimacst::bv_dimacst(
+  const namespacet &_ns,
+  dimacs_cnft &_prop,
+  message_handlert &message_handler,
+  const std::string &_filename)
+  : bv_pointerst(_ns, _prop, message_handler),
+    filename(_filename),
+    dimacs_cnf_prop(_prop)
+{
+}
+
 bool bv_dimacst::write_dimacs()
 {
   if(filename.empty() || filename == "-")
@@ -34,7 +45,7 @@ bool bv_dimacst::write_dimacs()
 
 bool bv_dimacst::write_dimacs(std::ostream &out)
 {
-  dynamic_cast<dimacs_cnft &>(prop).write_dimacs_cnf(out);
+  dimacs_cnf_prop.write_dimacs_cnf(out);
 
   // we dump the mapping variable<->literals
   for(const auto &s : get_symbols())
diff --git a/src/solvers/flattening/bv_dimacs.h b/src/solvers/flattening/bv_dimacs.h
index 9886cb125c3..248340f4d7f 100644
--- a/src/solvers/flattening/bv_dimacs.h
+++ b/src/solvers/flattening/bv_dimacs.h
@@ -14,17 +14,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bv_pointers.h"
 
+class dimacs_cnft;
+
 class bv_dimacst : public bv_pointerst
 {
 public:
   bv_dimacst(
     const namespacet &_ns,
-    propt &_prop,
+    dimacs_cnft &_prop,
     message_handlert &message_handler,
-    const std::string &_filename)
-    : bv_pointerst(_ns, _prop, message_handler), filename(_filename)
-  {
-  }
+    const std::string &_filename);
 
   virtual ~bv_dimacst()
   {
@@ -33,6 +32,8 @@ class bv_dimacst : public bv_pointerst
 
 protected:
   const std::string filename;
+  const dimacs_cnft &dimacs_cnf_prop;
+
   bool write_dimacs();
   bool write_dimacs(std::ostream &);
 };
diff --git a/src/solvers/sat/dimacs_cnf.cpp b/src/solvers/sat/dimacs_cnf.cpp
index 40f2a7c9f82..66b2587287b 100644
--- a/src/solvers/sat/dimacs_cnf.cpp
+++ b/src/solvers/sat/dimacs_cnf.cpp
@@ -37,13 +37,13 @@ dimacs_cnf_dumpt::dimacs_cnf_dumpt(
 {
 }
 
-void dimacs_cnft::write_dimacs_cnf(std::ostream &out)
+void dimacs_cnft::write_dimacs_cnf(std::ostream &out) const
 {
   write_problem_line(out);
   write_clauses(out);
 }
 
-void dimacs_cnft::write_problem_line(std::ostream &out)
+void dimacs_cnft::write_problem_line(std::ostream &out) const
 {
   // We start counting at 1, thus there is one variable fewer.
   out << "p cnf " << (no_variables()-1) << " "
@@ -76,7 +76,7 @@ void dimacs_cnft::write_dimacs_clause(
   out << "0" << "\n";
 }
 
-void dimacs_cnft::write_clauses(std::ostream &out)
+void dimacs_cnft::write_clauses(std::ostream &out) const
 {
   std::size_t count = 0;
   std::stringstream output_block;
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
index d938c7ce5ed..9eb44f806f5 100644
--- a/src/solvers/sat/dimacs_cnf.h
+++ b/src/solvers/sat/dimacs_cnf.h
@@ -20,7 +20,7 @@ class dimacs_cnft:public cnf_clause_listt
   explicit dimacs_cnft(message_handlert &);
   virtual ~dimacs_cnft() { }
 
-  virtual void write_dimacs_cnf(std::ostream &out);
+  virtual void write_dimacs_cnf(std::ostream &out) const;
 
   // dummy functions
 
@@ -36,8 +36,8 @@ class dimacs_cnft:public cnf_clause_listt
   write_dimacs_clause(const bvt &, std::ostream &, bool break_lines);
 
 protected:
-  void write_problem_line(std::ostream &out);
-  void write_clauses(std::ostream &out);
+  void write_problem_line(std::ostream &out) const;
+  void write_clauses(std::ostream &out) const;
 
   bool break_lines;
 };