How to invoke Z3 on an input file

Question

I have a file containing:

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)

and, according to the online tutorial, running z3 on this file should return:

sat
(model
    (define-fun c () Int
        (- 5))
    (define-fun a () Int
        0)
    (define-fun b () Int
        (- 3))
    (define-fun d ()
        Real 0.0)
    (define-fun e ()
        Real 0.0)
)

So I know this is legal Z3 input. However, whenever I run "z3 [option] " all I get is error messages no matter what option I choose -- including none. Can someone tell me how to correctly invoke Z3 on the input file?

Regards.