From 704dc9375d97358e5f293a5d7bc4de9955c44559 Mon Sep 17 00:00:00 2001
From: "Guangyu (Gary) HU" <43922980+Gy-Hu@users.noreply.github.com>
Date: Thu, 9 Apr 2026 17:01:07 +0800
Subject: [PATCH] mini_ic3: fix generalize() returning empty/init-overlapping
 core (#9245)

Two fixes in examples/python/mini_ic3.py:

1. generalize(): the polarity of the disjointness check was inverted,
   and there was no guard against an empty unsat core. With an empty
   core, And([])=True so check_disjoint(init, prev(True)) is always
   False (init is sat), and the code returned the empty core. That
   empty core then became cube2clause([])=Or([])=False, which got
   added as a lemma to all frames. The frame became inconsistent and
   is_valid() returned And(Or())=False as the "inductive invariant".

   Fix: require len(core) > 0 AND check_disjoint(init, prev(core))
   (without the spurious 'not'), so the core is only used when it
   is genuinely disjoint from init.

2. is_transition(): when an init rule's body happens to be an And
   without any Invariant predicate (e.g. (and (not A) (not B) ...)),
   is_body() returns (And(...), None). is_transition then passed
   inv0=None to subst_vars() which crashed inside get_vars(). Add an
   explicit None check so the rule falls through to is_init().

Verified on horn1..5 (unchanged behavior), h_CRC and h_FIFO from the
blocksys benchmarks (now correctly return CEX matching z3 spacer),
and cache_coherence_three (no longer collapses to (and or)).
---
 examples/python/mini_ic3.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/examples/python/mini_ic3.py b/examples/python/mini_ic3.py
index 31d3c595b..13056d385 100644
--- a/examples/python/mini_ic3.py
+++ b/examples/python/mini_ic3.py
@@ -74,6 +74,8 @@ class Horn2Transitions:
         pred, inv0 = self.is_body(body)
         if pred is None:
             return False
+        if inv0 is None:
+            return False
         inv1 = self.is_inv(head)
         if inv1 is None:
             return False
@@ -335,7 +337,7 @@ class MiniIC3:
         s = self.states[f - 1].solver
         if unsat == s.check(cube):
             core = s.unsat_core()
-            if not check_disjoint(self.init, self.prev(And(core))):
+            if len(core) > 0 and check_disjoint(self.init, self.prev(And(core))):
                 return core, f
         return cube, f