mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

assert before deref

Browse source
This commit is contained in:
Jakob Rath 2023-02-01 10:41:02 +01:00
parent 9314ad3808
commit 3c822117d1
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/conflict.cpp
View file

@ -303,15 +303,15 @@ namespace polysat {
} }
void conflict::add_lemma(char const* name, clause_ref lemma) { void conflict::add_lemma(char const* name, clause_ref lemma) {
if (!name)
name = "<unknown>";
LOG_H3("Lemma " << name << ": " << show_deref(lemma));
VERIFY(lemma);
for (auto lit : *lemma) for (auto lit : *lemma)
if (s.m_bvars.is_true(lit)) if (s.m_bvars.is_true(lit))
verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n"; verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
if (!name)
name = "<unknown>";
LOG_H3("Lemma " << name << ": " << show_deref(lemma));
SASSERT(lemma);
s.m_simplify_clause.apply(*lemma); s.m_simplify_clause.apply(*lemma);
lemma->set_redundant(true); lemma->set_redundant(true);
lemma->set_name(name); lemma->set_name(name);