#fix #5328

in-processing for "pure" PB constraints isn't model preserving and therefore removed.

src/sat/smt/pb_solver.cpp

@@ -132,7 +132,6 @@ namespace pb {
             remove_constraint(p, "is tight");
         }
         else {
-
             unsigned sz = p.size();
             clear_watch(p);
             unsigned j = 0;
@@ -1470,7 +1469,6 @@ namespace pb {
             return true;
         }
         else if (c.lit() != sat::null_literal && value(c.lit()) != l_true) {
-        // else if (c.lit() != sat::null_literal && value(c.lit()) == l_false) {
             return true;
         }
         else {
@@ -2025,7 +2023,7 @@ namespace pb {
             unit_strengthen();
             cleanup_clauses();
             cleanup_constraints();
-            update_pure();
+
             count++;
         }        
         while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size()));
@@ -2047,41 +2045,6 @@ namespace pb {
         // if (s().m_clauses.size() < 80000) lp_lookahead_reduction();
     }
 
-    /*
-     * ~lit does not occur in clauses
-     * ~lit is only in one constraint use list
-     * lit == C 
-     * -> ignore assignments to ~lit for C
-     * 
-     * ~lit does not occur in clauses
-     * lit is only in one constraint use list
-     * lit == C
-     * -> negate: ~lit == ~C
-     */
-    void solver::update_pure() {
-        //return;
-        for (constraint* cp : m_constraints) {
-            literal lit = cp->lit();
-            if (lit != sat::null_literal && 
-                !cp->is_pure() &&
-                value(lit) == l_undef && 
-                get_wlist(~lit).size() == 1 &&              
-                m_clause_use_list.get(lit).empty()) {
-                clear_watch(*cp);
-                cp->negate();
-                lit.neg();
-            }
-            if (lit != sat::null_literal && 
-                !cp->is_pure() &&
-                m_cnstr_use_list[(~lit).index()].size() == 1 &&
-                get_wlist(lit).size() == 1 && 
-                m_clause_use_list.get(~lit).empty()) { 
-                cp->set_pure();
-                get_wlist(~lit).erase(sat::watched(cp->cindex())); // just ignore assignments to false
-            }
-        }
-    }
-
     void solver::mutex_reduction() {
         literal_vector lits;
         for (unsigned v = 0; v < s().num_vars(); ++v) {

src/sat/tactic/sat_tactic.cpp

@@ -56,6 +56,12 @@ class sat_tactic : public tactic {
                   for (func_decl* f : funs) 
                       tout << mk_ismt2_pp(f, m) << "\n";
                   );
+
+            expr_ref_vector fmls_to_validate(m);
+            if (gparams::get_ref().get_bool("model_validate", false)) 
+                for (unsigned i = 0; i < g->size(); ++i) 
+                    fmls_to_validate.push_back(g->form(i));
+
             g->reset();
             g->m().compact_memory();
 
@@ -65,7 +71,8 @@ class sat_tactic : public tactic {
             dep2assumptions(dep2asm, assumptions);
             lbool r = m_solver->check(assumptions.size(), assumptions.data());
             TRACE("sat", tout << "result of checking: " << r << " "; 
-                  if (r == l_undef) tout << m_solver->get_reason_unknown(); tout << "\n";);
+                  if (r == l_undef) tout << m_solver->get_reason_unknown(); tout << "\n";
+                  if (m_goal2sat.has_interpreted_funs()) tout << "has interpreted\n";);
             if (r == l_false) {
                 expr_dependency * lcore = nullptr;
                 if (produce_core) {
@@ -106,6 +113,10 @@ class sat_tactic : public tactic {
                             break;
                         }
                     }
+                    for (auto* f : fmls_to_validate) 
+                        if (md->is_false(f)) 
+                            IF_VERBOSE(0, verbose_stream() << "failed to validate: " << mk_pp(f, m) << "\n";);
+
                     m_goal2sat.update_model(md);
                     TRACE("sat_tactic", model_v2_pp(tout, *md););
                     g->add(model2model_converter(md.get()));