Add an optimize test (#1230)

We do not check that optimization works with arithmetical expressions
in `maximize` or `minimize`.

(We do it for `ite` and bitvector expressions).

tests/models/arith/arith15.models.expected

@@ -0,0 +1,9 @@
+
+unknown
+(
+  (define-fun x () Int 5)
+  (define-fun y () Int 0)
+)
+(objectives 
+  ((- (* 5 x) y) 25)
+)

tests/models/arith/arith15.models.smt2

@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(assert (<= x 5))
+(assert (<= 0 y))
+(maximize (- (* 5 x) y))
+(check-sat)
+(get-model)
+(get-objectives)