From 2b48092541925a0f89f3cf83e3dceffc7486f513 Mon Sep 17 00:00:00 2001
From: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
Date: Sun, 23 Aug 2015 10:58:12 -0700
Subject: [PATCH] local sat solver change

Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
---
 src/sat/sat_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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();