我需要你的帮助，用 Z3 Java API 定义一个函数。我尝试解决这样的问题（在 z3.exe 进程中工作正常）：
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Bool)
(define-fun max2 ((x Real) (y Real)) Real (ite (<= x y) y x))
(assert (and (>= a 0.0) (<= a 100.0)))
(assert (or (= (max2 (+ 100.0 (* (- 1.0) a)) (/ 1.0 1000.0)) 0.0) c (not (= b 0.0))))
(check-sat-using (then simplify bit-blast qfnra))
(get-model)
此 smt 文件的结果是：
sat
(model
(define-fun a () Real
1.0)
(define-fun c () Bool
false) …