Opensmt rejects non-linear integer arithmetic too eagerly

[aehyvari]

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)

[blishko]

I think this is not going to be easy in the current implementation. The code of ArithLogic assumes we do not create nonlinear expressions.

I see two ways forward here, both of which would be good to have, eventually.
One is a change in the frontend, which would use a new term data structure that would follow closely the term grammar of SMT-LIB, and we would translate that to PTRef during some internalization process.
Second change is to actually start supporting nonlinear arithmetic, at least in the term representation.

[blishko]

We talked with @BritikovKI about this and I think we should start supporting nonlinear arithmetic expressions inArithLogic.
It would be a good step towards nonlinear arithmetic solver.