foldr (+) 0 [1,2,3]
foldr f z l = case l of [] -> z ; (x:xs) -> f x (foldr f z xs)
append(A,B,[1,2,3]).
append([],YS,YS). append([X|XS],YS,[X|ZS]):-append(XS,YS,ZS).
(set-logic QF_LIA) (set-option :produce-models true) (declare-fun a () Int) (declare-fun b () Int) (assert (and (>= a 5) (<= b 30) (= (+ a b) 20))) (check-sat) (get-value (a b))