From aa5645b54bea707f16935ae8b87b849995ee29fd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Oct 2025 13:22:18 -0700 Subject: [PATCH] fixing the order Signed-off-by: Lev Nachmanson --- src/ast/normal_forms/nnf.cpp | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 4de3d7ba7..746d48fa2 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -566,7 +566,8 @@ struct nnf::imp { expr * _then = rs[2]; expr * _else = rs[3]; - app * r = m.mk_and(m.mk_or(_not_cond, _then), m.mk_or(_cond, _else)); + expr* a = m.mk_or(_not_cond, _then); + app * r = m.mk_and(a, m.mk_or(_cond, _else)); m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -612,11 +613,13 @@ struct nnf::imp { app * r; if (is_eq(t) == fr.m_pol) { - auto a = m.mk_or(not_lhs, rhs); + expr* 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)); + else { + expr* a = m.mk_or(lhs, rhs); + r = m.mk_and(a, m.mk_or(not_lhs, not_rhs)); + } m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -688,8 +691,8 @@ struct nnf::imp { if (proofs_enabled()) { expr_ref aux(m); aux = m.mk_label(true, names.size(), names.data(), arg); - pr = m.mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)), - m.mk_iff_oeq(m.mk_rewrite(aux, r))); + auto a = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)); + pr = m.mk_transitivity(a, m.mk_iff_oeq(m.mk_rewrite(aux, r))); } } else {