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