diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3d6130d5e..8761873bc 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2626,7 +2626,7 @@ namespace sat {
         out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
 
         for (unsigned i = 0; i < m_trail.size(); i++) {
-            out << dimacs_lit(m_trail[i]) << " 0\n";
+            out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n";
         }
         vector<watch_list>::const_iterator it  = m_watches.begin();
         vector<watch_list>::const_iterator end = m_watches.end();