关于(check-sat)与(get-model)的标记疑问：如何实现无报错标记？

首先得明确：你不能直接在未确认(check-sat)返回sat的情况下调用(get-model)——这是SMT-LIB标准规定的行为，当求解结果是unsat或unknown时，(get-model)本身就是非法调用，所以报错是预期的，不存在“无报错执行标记+调用get-model”的方法（除非结果是sat，但那时候你也不需要标记no sat了）。

正确的处理流程 #

解决这个问题的核心思路是先执行(check-sat)并获取结果，再根据结果分支处理：

• 如果(check-sat)返回sat：再调用(get-model)获取模型
• 如果(check-sat)返回unsat：直接执行你的标记操作，跳过(get-model)

举个实际的例子，不管是用交互模式还是编程语言API，都要遵循这个逻辑：

1. SMT-LIB交互模式示例

(declare-const x Int)
(assert (> x 5))
(assert (< x 3))
(check-sat) ; 这里会返回unsat
; 此时执行你的标记操作（比如记录日志、设置状态等）
; 不要调用(get-model)，否则会触发报错

2. Z3 Python API示例

from z3 import *

# 构建约束
x = Int("x")
solver = Solver()
solver.add(x > 5, x < 3)

# 先检查可满足性
result = solver.check()

if result == sat:
    # 有模型，获取并处理
    print("模型:", solver.model())
elif result == unsat:
    # 无满足解，执行标记操作
    print("标记为no sat")
else:
    # 结果未知的情况
    print("无法确定可满足性")

为什么会报错？ #

根据SMT-LIB 2.0+的规范，(get-model)只有在(check-sat)返回sat时才是合法的。当结果是unsat时，不存在任何满足约束的模型，求解器自然无法返回模型，所以会直接抛出错误——这不是求解器的bug，是必须遵守的规则。

所以结论是：必须先通过(check-sat)确认结果为sat，再调用(get-model)；如果是unsat，直接执行标记操作即可，这样既不会报错，也能实现你想要的标记逻辑。

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