The tutorial has this as example input:
(set-option :produce-models true)
(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= (+ x y) 9))
(assert (= (+ (* 2 x) (* 3 y)) 22))
(check-sat)
(get-value (x))
(get-value ((- x y) (+ 2 y)))
And indicates this should be the output:
sat
((x 5))
(((- x y) 1) ((+ 2 y) 8))
But either the 8 should be a 6, or the + a *
PS: I can't find the source of the tutorial