From 618d394ab59f14860939f1ccfdc5cf9ffc229b72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 May 2018 09:41:12 +0100 Subject: [PATCH] unreferenced variables Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 1 - src/smt/theory_pb.cpp | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) 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; }