From 8938de2ba2a8ae33f031c8e0b3dc422a5ff93a4b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Aug 2014 12:11:34 -0700
Subject: [PATCH] fix build error reported by Ari

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxhs.h     | 2 +-
 src/sat/sat_mus.cpp | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/opt/maxhs.h b/src/opt/maxhs.h
index 6bb7a2696..f31cbce9f 100644
--- a/src/opt/maxhs.h
+++ b/src/opt/maxhs.h
@@ -24,6 +24,6 @@ Notes:
 
 namespace opt {
     maxsmt_solver_base* mk_maxhs(context& c,
-                                 vector<rational> const& ws, expr_ref_vector const& soft);
+                                 weights_t& ws, expr_ref_vector const& soft);
 }
 #endif
diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp
index 74f17f8ea..b33c9420c 100644
--- a/src/sat/sat_mus.cpp
+++ b/src/sat/sat_mus.cpp
@@ -71,7 +71,7 @@ namespace sat {
             literal lit = core.back();
             core.pop_back();
             unsigned sz = mus.size();
-            mus.push_back(~lit); // TBD: measure
+            // mus.push_back(~lit); // TBD: measure
             mus.append(core);
             lbool is_sat = s.check(mus.size(), mus.c_ptr());
             TRACE("sat", tout << "mus: " << mus << "\n";);