mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-15 17:52:33 -07:00
parent 715081cbd1
commit 305c1c1dc2
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -150,7 +150,7 @@ class skolemizer {
p = nullptr;
if (m_proofs_enabled) {
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
p = m.mk_skolemization(q, r);
}
@ -645,7 +645,6 @@ struct nnf::imp {
m_result_stack.push_back(n2);
if (proofs_enabled()) {
if (!fr.m_pol) {
verbose_stream() << mk_pp(t, m) << "\n";
proof * prs[1] = { pr2 };
pr2 = m.mk_oeq_congruence(m.mk_not(t), static_cast<app*>(n2.get()), 1, prs);
}