NIA reasonning too weak

[iguerNL]

The following formula is unsat:

(declare-fun s () Int)
(declare-fun y () Int)
(declare-fun th () Int)

(assert (> s 0))
(assert (>= s (+ (* y s) 1)))
(assert (>= (* y s) 10))

(check-sat)

But Alt-Ergo returns "unkown" on it. When asked to produce a model, it loops (in the case-split engine)