diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 248e783e5..953b1979f 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -3122,13 +3122,11 @@ namespace smt2 { m_num_bindings = 0; m_num_open_paren = 0; - unsigned found_errors = 0; try { scan_core(); parse_sort(context); - if (!sort_stack().empty()) { + if (!sort_stack().empty()) return sort_ref(sort_stack().back(), m()); - } } catch (z3_exception & ex) { error(ex.msg()); diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index eab37066e..b56f4efb1 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -177,7 +177,7 @@ namespace array { TRACE("array", tout << "can beta reduce " << can_beta_reduce(child) << "\n";); if (can_beta_reduce(child)) push_axiom(select_axiom(select, child)); - propagate_parent_select_axioms(v_child); + propagate_parent_select_axioms(v_child); } void solver::add_lambda(theory_var v, euf::enode* lambda) { diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index e3c193f5a..e8e4305d0 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -653,9 +653,8 @@ namespace bv { if (!argn->is_attached_to(get_id())) { mk_var(argn); } - theory_var v_arg = argn->get_th_var(get_id()); - unsigned arg_sz = get_bv_size(v_arg); - SASSERT(idx < arg_sz); + theory_var v_arg = argn->get_th_var(get_id()); + SASSERT(idx < get_bv_size(v_arg)); sat::literal lit = expr2literal(n); sat::literal lit0 = m_bits[v_arg][idx]; if (lit0 == sat::null_literal) { diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 6cb889ee1..66daf07ea 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -84,7 +84,7 @@ namespace q { clause& m_clause; euf::enode* const* m_binding; justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, euf::enode_pair* ev): - m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_clause(c), m_binding(b), m_num_ev(n), m_evidence(ev) {} + m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ev(n), m_evidence(ev), m_clause(c), m_binding(b) {} sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); } diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index f1ae29586..1dba2e768 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -206,6 +206,8 @@ public: std::istringstream istrm(ostrm.str()); params_ref p; auto srt = parse_smt2_sort(ctx, istrm, false, p, "quantifier"); + if (!srt) + goto bail; names.push_back(name); domain.push_back(srt); } @@ -215,7 +217,6 @@ public: sexpr->display(std::cout); std::cout << "\n"; exit(0); - } void parse_sexpr(sexpr_ref const& sexpr, cmd_context& ctx, expr_ref_vector const& args, expr_ref& result) { @@ -428,4 +429,4 @@ unsigned read_drat(char const* drat_file, char const* problem_file) { } verify_smt(drat_file, problem_file); return 0; -} \ No newline at end of file +} diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 47bc13242..14a71ae28 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -315,7 +315,7 @@ namespace smt { void conflict_resolution::process_antecedent(literal antecedent, unsigned & num_marks) { bool_var var = antecedent.var(); unsigned lvl = m_ctx.get_assign_level(var); - SASSERT(var < static_cast(m_ctx.get_num_bool_vars())); + SASSERT(var < m_ctx.get_num_bool_vars()); TRACE("conflict_", tout << "processing antecedent (level " << lvl << "):"; m_ctx.display_literal(tout, antecedent); m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ba9f7c8fd..e9e80efcb 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1558,7 +1558,6 @@ bool theory_seq::check_ubv_string() { } bool theory_seq::check_ubv_string(expr* e) { - expr* n = nullptr; if (ctx.inconsistent()) return true; if (m_has_ubv_axiom.contains(e)) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index e5c1469a6..6705d40e4 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -5523,6 +5523,7 @@ namespace smt { TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;); if (groundedMap.find(node) != groundedMap.end()) { for (auto const &itor : groundedMap[node]) { + (void) itor; TRACE("str", tout << "\t[grounded] "; for (auto const &vIt : itor.first) { diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index 57edce73d..ac6cdede2 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -50,7 +50,6 @@ class solver_subsumption_tactic : public tactic { return false; expr_ref_vector ors(m); ors.append(to_app(f)->get_num_args(), to_app(f)->get_args()); - unsigned j = 0; expr_ref_vector prefix(m); for (unsigned i = 0; i < ors.size(); ++i) { expr_ref_vector fmls(m); @@ -124,9 +123,15 @@ public: ~solver_subsumption_tactic() override {} - void updt_params(params_ref const& p) override { m_params = p; } + void updt_params(params_ref const& p) override { + m_params = p; + unsigned max_conflicts = p.get_uint("max_conflicts", 2); + m_params.set_uint("sat.max_conflicts", max_conflicts); + m_params.set_uint("smt.max_conflicts", max_conflicts); + } void collect_param_descrs(param_descrs& r) override { + r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call."); } void operator()(goal_ref const& g, goal_ref_buffer& result) override {