mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 03:41:21 +00:00
Code Activity

#6696

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-13 21:48:46 -07:00
parent dda9242616
commit a8da0a6851
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), m.mk_not(r)); p = m.mk_skolemization(mk_not(m, q), mk_not(m, r));
else else
p = m.mk_skolemization(q, r); p = m.mk_skolemization(q, r);
} }