SMTLIB2 parser (tokenizer) wrongly rejects set-logic commands and has a non-helpful error message for parse() for > 1 items

[baierd]

Our SMTLIB2 parser, to be exact its tokenizer, rejects set-logic commands that are not at the very beginning of the SMT-LIB2 file. This is wrong. these commands are allowed to be everywhere in the file and may be repeated with certain settings. set-logic has 2 restrictions; it may not be used again as long as the reset command has not been used, and it must be used before any define-*, declare-*, or assert commands are used. But many solvers don't stick to this, leading to us usually implicitly assuming that the ALL logic is set.
For benchmarks the set-info command required to be in the very first line (or to be the first command?), and it needs to set the :smt-lib-version attribute. But this is nothing we can or should require, as not everything is a benchmark.

Also, the parse() method returns a not so helpful exception if there is more than 1 returned formula.