diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 2e16bc33e..e1e0e0b0a 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -871,6 +871,5 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof
 
 tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) {
     parallel_params pp(p);
-    bool use_parallel = pp.enable();
     return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p) : mk_sat_tactic(m);
 }
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index d1ac608ea..1e5b35fbf 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -2504,7 +2504,7 @@ namespace smt {
     bool theory_pb::validate_unit_propagation(card const& c) {
         context& ctx = get_context();
         for (unsigned i = c.k(); i < c.size(); ++i) {
-            SASSERT(ctx.get_assignment(c.lit(i)) == l_false);
+            VERIFY(ctx.get_assignment(c.lit(i)) == l_false);
         }
         return true;
     }