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

fix #6689

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-17 12:05:08 -07:00
parent 1319b64bb0
commit cb041c1b6d
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/normal_forms/nnf.cpp
View file

@ -149,7 +149,7 @@ class skolemizer {
p = nullptr; p = nullptr;
if (m_proofs_enabled) { if (m_proofs_enabled) {
if (q->get_kind() == forall_k) if (q->get_kind() == forall_k)
p = m.mk_skolemization(mk_not(m, q), mk_not(m, r)); p = m.mk_skolemization(mk_not(m, q), m.mk_not(r));
else else
p = m.mk_skolemization(q, r); p = m.mk_skolemization(q, r);
} }