mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

lemma

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 14:46:35 +02:00
parent 8edcb9e268
commit cf80225fee
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -219,11 +219,13 @@ namespace polysat {
clause_builder lemma(s()); clause_builder lemma(s());
for (auto c : m_constraints) { for (auto c : m_constraints) {
if (!c->has_bvar()) SASSERT(!c->has_bvar());
keep(c); keep(c);
lemma.push(~c);
} }
for (auto c : *this)
lemma.push(~c);
for (unsigned v : m_vars) { for (unsigned v : m_vars) {
if (!is_pmarked(v)) if (!is_pmarked(v))
continue; continue;