From b9be33bb06b5e29ab65963e87c32bfa5c8a7f701 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 29 Apr 2026 17:18:45 -0700
Subject: [PATCH] Reorder null check before side effect in
 `linearise_multi_pattern` (#9427)

* Initial plan

* Move null check before side effect in linearise_multi_pattern

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/cc69d451-b5a7-414d-9154-2cda3286fe40

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/mam.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index a647a2a71..006cb2697 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1114,9 +1114,9 @@ namespace {
                         best_j         = j;
                     }
                 }
-                m_mp_already_processed[best_j] = true;
                 if (best == nullptr)
                     continue;
+                m_mp_already_processed[best_j] = true;
                 app * p                 = best;
                 func_decl * lbl         = p->get_decl();
                 unsigned short num_args = p->get_num_args();