#5454

Z3Prover · Aug 11, 2021 · d1d64bb · d1d64bb
1 parent 4f2211b
commit d1d64bb
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 12 deletions.
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
@@ -2022,10 +2022,14 @@ namespace sat {
         }
         remove_bin_clauses(pos_l);
         remove_bin_clauses(neg_l);
-        remove_clauses(pos_occs, pos_l);
-        remove_clauses(neg_occs, neg_l);
-        pos_occs.reset();
-        neg_occs.reset();
+        {
+            clause_use_list& pos_occs = m_use_list.get(pos_l);
+            clause_use_list& neg_occs = m_use_list.get(neg_l);
+            remove_clauses(pos_occs, pos_l);
+            remove_clauses(neg_occs, neg_l);
+            pos_occs.reset();
+            neg_occs.reset();
+        }
         return true;
     }
 

diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp
@@ -53,7 +53,7 @@ class solver_subsumption_tactic : public tactic {
     */
 
     bool simplify(expr_ref& f) {
-        expr_ref_vector fmls(m), ors(m), nprefix(m), prefix(m);
+        expr_ref_vector fmls(m), ors(m), nors(m), prefix(m);
         expr_ref nf(m.mk_not(f), m);
         fmls.push_back(nf);
         lbool is_sat = m_solver->check_sat(fmls);
@@ -65,15 +65,15 @@ class solver_subsumption_tactic : public tactic {
             return false;
         ors.append(to_app(f)->get_num_args(), to_app(f)->get_args());
         for (expr* arg : ors)
-            nprefix.push_back(mk_not(m, arg));
+            nors.push_back(mk_not(m, arg));
         for (unsigned i = 0; i < ors.size(); ++i) {
             expr* arg = ors.get(i);
-            expr_ref save(nprefix.get(i), m);
-            nprefix[i] = arg;
-            is_sat = m_solver->check_sat(nprefix);
-            nprefix[i] = save;
+            expr_ref save(nors.get(i), m);
+            nors[i] = arg;
+            is_sat = m_solver->check_sat(nors);
+            nors[i] = save;
             if (is_sat == l_false) 
-                nprefix[i] = m.mk_true();
+                nors[i] = m.mk_true();
             else 
                 prefix.push_back(arg);            
         }
@@ -141,7 +141,7 @@ class solver_subsumption_tactic : public tactic {
     }
 
     void collect_param_descrs(param_descrs& r) override { 
-        r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call.");
+        r.insert("max_conflicts", CPK_UINT, "(default: 2) maximal number of conflicts allowed per solver call.");
     }
 
     void operator()(goal_ref const& g, goal_ref_buffer& result) override {