They contain the undefined "const" operator

- Move benchmarks mixing Int and Real to non-standard
- Move benchmarks containing not-strictly linear expressions to
  QF_NRA

For the sake of syntax highlighting

Change logic of these benchmarks according to the output of
Dolmen and yices2. Yices2 was used for a few very big benchmarks.