From cb041c1b6d43208597744233bfca90ae7340927d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 17 Apr 2023 12:05:08 -0700
Subject: [PATCH] fix #6689

---
 src/ast/normal_forms/nnf.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index a35956454..b04445d16 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -149,7 +149,7 @@ class skolemizer {
         p = nullptr;
         if (m_proofs_enabled) {
             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
                 p = m.mk_skolemization(q, r);
         }