При следния SMT2 скрипт:
(set-option :produce-proofs true)
(set-logic AUFLIRA)
(declare-sort Complex$ 0)
(declare-fun r$ () Real)
(declare-fun s$ () Complex$)
(declare-fun re$ (Complex$) Real)
(declare-fun norm$ (Complex$) Real)
(assert (! (not (=> (and (forall ((?v0 Complex$)) (<= (ite (< (re$ ?v0) 0.0) (- (re$ ?v0)) (re$ ?v0)) (norm$ ?v0))) (<= (norm$ s$) r$)) (<= (ite (< (re$ s$) 0.0) (- (re$ s$)) (re$ s$)) (+ r$ 1.0)))) :named a0))
(check-sat)
(get-proof)
Z3 (нестабилна версия) създава доказателство, което съдържа функция на Skolem "norm$0". Тази функция се въвежда в стъпка на пренаписване:
(ALL v0. (if 0 <= Re v0 then Re v0 else - 1 * Re v0) <= cmod v0) =
((ALL v0. cmod v0 = (if 0 <= Re v0 then Re v0 else - 1 * Re v0) + norm_0 v0) & (ALL v0. 0 <= norm_0 v0))
Може ли това поведение да бъде потиснато от превключвател на командния ред? Тоест, има ли вариант Z3 да изведе доказателство без такава функция Skolem? Това по принцип трябва да е възможно, тъй като Z3 версия 3.2 намира доказателство, което не изисква функция Skolem.
