Jasper Yu says to YSITD @koru1130 相等於你剛剛在用的那個 (declare-fun x () Int) (assert (> x 0)) (check-sat) (get-model) (exit)