mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

fix validator bug returning true for unprocessed case, bug reported in #6116

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-23 20:17:32 -07:00
parent ce1f3987d9
commit c6263587c3
3 changed files with 14 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/euf_solver.cpp
View file

@ -355,8 +355,7 @@ namespace euf {
if (m_relevancy.enabled()) if (m_relevancy.enabled())
m_relevancy.propagate(); m_relevancy.propagate();
if (m_egraph.inconsistent()) { if (m_egraph.inconsistent()) {
unsigned lvl = s().scope_lvl(); set_conflict(conflict_constraint().to_index());
s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index()));
return true; return true;
} }
bool propagated1 = false; bool propagated1 = false;

21
src/sat/smt/q_ematch.cpp
View file

@ -372,21 +372,18 @@ namespace q {
} }
void ematch::propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx) { 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; ++m_stats.m_num_conflicts;
ctx.set_conflict(j_idx); else
}
else {
++m_stats.m_num_propagations; ++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() { bool ematch::flush_prop_queue() {

5
src/shell/drat_frontend.cpp
View file

@ -250,13 +250,14 @@ public:
std::cout << "p hint verified\n"; std::cout << "p hint verified\n";
return true;
break; break;
} }
default: default:
UNREACHABLE(); UNREACHABLE();
break; break;
} }
return true; return false;
} }
/** /**
@ -459,7 +460,7 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
std::cout.flush(); std::cout.flush();
switch (r.m_tag) { switch (r.m_tag) {
case dimacs::drat_record::tag_t::is_clause: { 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); checker.add(r.m_lits, r.m_status, validated);
if (drat_checker.inconsistent()) { if (drat_checker.inconsistent()) {
std::cout << "inconsistent\n"; std::cout << "inconsistent\n";