在本文（第 3.2 节）中，它说 z3 在执行任何其他步骤之前应用了公式的重写/简化。
假设我有一个公式QF_UF，它由多个assert语句组成。是否有任何重写规则会以某种方式“打破”不同断言语句之间的障碍？或者，反过来问：我可以确定重写规则只在本地应用，“在”一个断言语句中？
例如，考虑以下公式：
(set-logic QF_UF)
(set-option :auto-config false)
(set-option :PROOF_MODE 2)
(declare-fun a () Bool)
(assert a)
(assert (not a))
(check-sat)
(get-proof)
我可以确定证明将包含一个解决步骤来证明False，或者是否有可能False通过重写/简化步骤来结束？
我问的原因是对于我的应用程序，每个assert语句都有一个特殊的语义。对多个assert语句进行重写/简化将使最终的不可满足性证明对我来说无法使用（或至少：非常难以使用）。