cleanups

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

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) {

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());
+        theory_var v_arg = argn->get_th_var(get_id());        
-        unsigned arg_sz = get_bv_size(v_arg);
+        SASSERT(idx < get_bv_size(v_arg));
-        SASSERT(idx < arg_sz);
         sat::literal lit = expr2literal(n);
         sat::literal lit0 = m_bits[v_arg][idx];
         if (lit0 == sat::null_literal) {

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

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;
-}
+}

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

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

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) {

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 {