Opensmt rejects non-linear integer arithmetic too eagerly 

Opensmt throws a `LANonLinearException` on this instance.  It'd be nice if it didn't.  Maybe we should somehow tell `ArithLogic` when it is parsing a `define-fun` to ignore the nonlinearities.

```
(set-logic QF_LIA)
(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
(assert (= (uninterp_mul 1 2)))
(check-sat)
(exit)
```