fix validator bug returning true for unprocessed case, bug reported in …

…#6116
Z3Prover · Aug 24, 2022 · c626358 · c626358
1 parent ce1f398
commit c626358
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 17 deletions.
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -355,8 +355,7 @@ namespace euf {
             if (m_relevancy.enabled())
                 m_relevancy.propagate();
             if (m_egraph.inconsistent()) {  
-                unsigned lvl = s().scope_lvl();
-                s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index()));
+                set_conflict(conflict_constraint().to_index());
                 return true;
             }
             bool propagated1 = false;

diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
@@ -372,21 +372,18 @@ namespace q {
     }
 
     void ematch::propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx) {
-        if (is_conflict) {
+        if (is_conflict) 
             ++m_stats.m_num_conflicts;
-            ctx.set_conflict(j_idx);
-        }
-        else {
+        else
             ++m_stats.m_num_propagations;
-            auto& j = justification::from_index(j_idx);
-            sat::literal_vector lits;
-            lits.push_back(~j.m_clause.m_literal);
-            for (unsigned i = 0; i < j.m_clause.size(); ++i) 
-                lits.push_back(instantiate(j.m_clause, j.m_binding, j.m_clause[i]));            
-            m_qs.log_instantiation(lits);
-            m_qs.add_clause(lits);
-        }
-
+
+        auto& j = justification::from_index(j_idx);
+        sat::literal_vector lits;
+        lits.push_back(~j.m_clause.m_literal);
+        for (unsigned i = 0; i < j.m_clause.size(); ++i) 
+            lits.push_back(instantiate(j.m_clause, j.m_binding, j.m_clause[i]));            
+        m_qs.log_instantiation(lits);
+        m_qs.add_clause(lits);               
     }
 
     bool ematch::flush_prop_queue() {

diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp
@@ -250,13 +250,14 @@ class smt_checker {
 
 
             std::cout << "p hint verified\n";
+            return true;
             break;
         }
         default:
             UNREACHABLE();
             break;
         }
-        return true;
+        return false;
     }
 
     /**
@@ -459,7 +460,7 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
         std::cout.flush();
         switch (r.m_tag) {
         case dimacs::drat_record::tag_t::is_clause: {
-            bool validated = false && checker.validate_hint(exprs, r.m_lits, r.m_hint);
+            bool validated = checker.validate_hint(exprs, r.m_lits, r.m_hint);
             checker.add(r.m_lits, r.m_status, validated);
             if (drat_checker.inconsistent()) {
                 std::cout << "inconsistent\n";