From 9b88aaf13468b2455a3f1295afe8ec4c521f56e9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 16 Sep 2025 16:32:46 -0700 Subject: [PATCH] determine parameter evaluation order Signed-off-by: Lev Nachmanson --- src/ast/normal_forms/nnf.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 3ca15ded8..4de3d7ba7 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -149,8 +149,10 @@ class skolemizer { r = m_subst(body, substitution); p = nullptr; if (m_proofs_enabled) { - if (q->get_kind() == forall_k) - p = m.mk_skolemization(mk_not(m, q), mk_not(m, r)); + if (q->get_kind() == forall_k) { + auto a = mk_not(m, q); + p = m.mk_skolemization(a , mk_not(m, r)); + } else p = m.mk_skolemization(q, r); } @@ -609,8 +611,10 @@ struct nnf::imp { expr * not_rhs = rs[3]; app * r; - if (is_eq(t) == fr.m_pol) - r = m.mk_and(m.mk_or(not_lhs, rhs), m.mk_or(lhs, not_rhs)); + if (is_eq(t) == fr.m_pol) { + auto a = m.mk_or(not_lhs, rhs); + r = m.mk_and(a, m.mk_or(lhs, not_rhs)); + } else r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs)); m_result_stack.shrink(fr.m_spos);