Z3求解器返回Unknown异常咨询：定义不当函数的SMT验证问题

Let's break down why Z3 is returning unknown instead of unsat here, and how to fix it.

The Core Issue: Missing Quantifier Instantiation #

Your expected proof hinges on instantiating both AX-1 and AX-2 for s=emp, but Z3 isn't triggering AX-1's instantiation—even though wild(emp) is present in your assertion. Here's the breakdown:

1. Trigger Limitations in AX-1
   AX-1 uses only (wild s) as its trigger. This means Z3 will only instantiate AX-1 when it encounters a term matching wild(s) (like wild(emp) in your assertion). However, after Z3 instantiates AX-2 (triggered by the same wild(emp) term), it rewrites wild(emp) to 1 + wild%limited(emp) in the context. Z3's heuristic doesn't re-scan for the wild(s) trigger once the original term is rewritten, so AX-1 never gets instantiated for s=emp.

2. Disabled Model-Based Quantifier Instantiation (MBQI)
   You turned off :smt.mbqi, which is Z3's mechanism for checking if a model can satisfy all quantifiers. Without MBQI, Z3 relies entirely on trigger-based instantiation. Since AX-1 isn't instantiated, Z3 can't detect the inherent contradiction between AX-1 and AX-2 (which would require wild%limited(emp) = 1 + wild%limited(emp)—a direct logical impossibility).

Fixes to Trigger the Correct Instantiations #

Option 1: Add a Dual Trigger to AX-1

Modify AX-1 to include a trigger for wild%limited(s) as well. This ensures that when wild%limited(emp) appears (after AX-2 is instantiated), Z3 will trigger AX-1's instantiation for s=emp:

(assert (forall ((s Snap)) (! ;; AX-1
  (= (wild%limited s) (wild s))
  :pattern ((wild s) (wild%limited s))  ;; Add wild%limited(s) as an additional trigger
)))

With this change, Z3 will:

• Instantiate AX-2 when it sees wild(emp), getting wild(emp) = 1 + wild%limited(emp)
• Instantiate AX-1 when it sees wild%limited(emp), getting wild%limited(emp) = wild(emp)
• Combine these to derive wild%limited(emp) = 1 + wild%limited(emp), a clear contradiction, leading to unsat.

Option 2: Re-enable MBQI

If you prefer not to adjust triggers, turning MBQI back on allows Z3 to detect the contradiction without relying solely on trigger-based instantiation. Remove the (set-option :smt.mbqi false) line, or set it to true:

(set-option :smt.mbqi true)

MBQI will attempt to construct a model for your axioms and quickly discover that no integer value for wild%limited(emp) can satisfy both AX-1 and AX-2, resulting in unsat.

内容的提问来源于stack exchange，提问作者Malte Schwerhoff