From eae4de075bb8e32b6c9963078af95c2049fcfe61 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 23 Sep 2025 10:47:24 +0300
Subject: [PATCH] fix latent bug in factorization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_basics_lemmas.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index 20d6cde75..b2c8e94c1 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -663,6 +663,8 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const
 // x = 0 or y = 0 -> xy = 0
 void basics::basic_lemma_for_mon_non_zero_model_based(const monic& rm, const factorization& f) {
     TRACE(nla_solver_bl, c().trace_print_monic_and_factorization(rm, f, tout););
+    if (!f.is_mon())
+        return;
     for (auto j : f) {
         if (val(j).is_zero()) {
             lemma_builder lemma(c(), "x = 0 => x*... = 0");