Terms as coefficients in QF_UFLRA and QF_UFLIA

[hansjoergschurr]

The logic definition for QF_UFLRA states the following about the allowed terms (a similar restriction exists for QF_UFLIA):

Terms with _concrete_ coefficients are also allowed, that is, terms
  of the form c, (* c x), or (* x c)  where x is a free constant and 
  c is an integer or rational coefficient. 
  - An integer coefficient is a term of the form m or (- m) for some
    numeral m.
  - A rational coefficient is a term of the form d, (- d) or (/ c n) 
    for some decimal d, integer coefficient c and numeral n other than 0.

I interpret this as saying that terms like (* 5 (f 0)) are not allowed. However, we have some old benchmarks that use this.
Eg. in incremental/QF_UFLIA/kind/metros_4.ec.smt2_4.ec.smt2 we have:

(assert (= (+ (___z8z___ 0) (+ (* (- 1) (___z7z___ 0)) (___z10z___ 0))) 0))

I believe the language definition is slightly too restrictive here. It should allow x to be more than a free constant.

[Gbury]

I agree. We could actually at the same time both accept more things as linear and simplify the spec by specifying that in linear arithmetic at least (and not exactly) one of the two operands is a coefficient/literal.