[SMT-LIB] Benchmarks Compliant to SMTLIB

[Paulo J. Matos]

Hello all,

I have seen some benchmarks (/sal) in QF_LRA, that contain terms of
the form: (* (- x10 x11) 10). This doesn't seem to comply with the
smtlib official syntax for QF_LRA, right?

<time to read the file>
I have just re-read the syntax for QF_LRA:
:extensions
 "Terms with positive integer coefficients are allowed, that is, expressions
  of the form (* n t) or (* t n) for some numeral n, both of which abbreviate
  the term (+ t ... t) having n occurrences of t.
 "

I would assume that it complies because it would be equivalent to (+
(- x10 x11) (- x10 x11) (- x10 x11) ...) , however, would this be
compliant: (* (- x10 x11) (/ 1 10))? It shouldn't because it says n
should be a numeral, right?

Cheers,
-- 
Paulo Jorge Matos - pocm at ecs.soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK