SMT_Answer

(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (and (or (< x0 10) (= x0 10)) (= x1 (- x0 1))) (and (= x2 x1) (= x2 9) ) ))
(check-sat)

output:sat

(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (> x0 10) (and (= x2 x0) (= x2 9) ) ))
(check-sat)

output:unsat

所以是整個logic formula是滿足的 , 代表有個int value會使執行時出現assert的錯誤訊息

就是x=10的時候