z3 maximization fails to infinity on simple model

I'm a beginner with z3 and I want use it to solve ILP problems. I've started with a very simple maximization problem like below:

(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(declare-const x3 Int)

(assert (= x0 1))
(assert (= x0 (+ x1 x2)))
(assert (= x3 (+ x1 x2)))

(maximize (+
    (* x0 5)
    (* x1 10)
    (* x2 6)
    (* x3 9)
))


(check-sat)
(get-objectives)
(get-model)

While the maximized solution should be 24, I get +oo:

sat
(objectives
 ((+ (* x0 5) (* x1 10) (* x2 6) (* x3 9)) oo)
)
(
  (define-fun x2 () Int
    0)
  (define-fun x3 () Int
    1)
  (define-fun x1 () Int
    1)
  (define-fun x0 () Int
    1)
)

With another even simpler problem, I get the right solution :

(declare-const x Int)
(declare-const y Int)
(assert (< x 2))
(assert (< (- y x) 1))
(maximize (+ x y))
(check-sat)
(get-model)
(get-objectives)

We get:

sat
(
  (define-fun x () Int
    1)
  (define-fun y () Int
    1)
)
(objectives
 ((+ x y) 2)
)

I can't figure out what is the difference ? Thanks your help.