620 smtlib2 parser tokenizer wrongly rejects set logic commands and has a non helpful error message for parse for 1 items

src/org/sosy_lab/java_smt/api/FormulaManager.java

@@ -193,6 +193,9 @@ default BooleanFormula makeDistinct(Formula... pArgs) {
   default BooleanFormula parse(String s) throws IllegalArgumentException {
     List<BooleanFormula> formulas = parseAll(s);
     checkArgument(!formulas.isEmpty(), "No assertion found in the SMTLIB string.");
+    checkArgument(
+        formulas.size() == 1,
+        "More than one assertion found in the SMT-LIB string, " + "please use parseAll(String).");
     return Objects.requireNonNull(Iterables.getOnlyElement(formulas));
   }
 

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

@@ -399,9 +399,17 @@ private String sanitize(String formulaStr) {
     int pos = 0; // index of the current token
 
     for (String token : tokens) {
-      if (Tokenizer.isSetLogicToken(token)) {
-        // Skip the (set-logic ...) command at the beginning of the input
-        Preconditions.checkArgument(pos == 0);
+      if (pos == 0 && Tokenizer.isSetInfoToken(token)) {
+        // set-info call is allowed to be the very first command in the benchmark, but can also
+        // appear repeatedly throughout a SMT2 program
+        // Technically it is even required to be the very first command, and it must set the
+        //  :smt-lib-version attribute. See SMT-LIB 2.7 §3.11.3
+        // TODO: check that version >= 2?
+        Preconditions.checkArgument(token.contains(":smt-lib-version"));
+
+      } else if (Tokenizer.isSetLogicToken(token)) {
+        // Skip (set-logic ...) commands for now. They may appear throughout an SMT-LIB2 program
+        // to set the 'current logic' to a new logic. Default (no command needed): ALL.
 
       } else if (Tokenizer.isExitToken(token)) {
         // Skip the (exit) command at the end of the input

src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java

@@ -155,6 +155,10 @@ public static boolean isSetLogicToken(String token) {
     return matchesOneOf(token, "set-logic");
   }
 
+  public static boolean isSetInfoToken(String token) {
+    return matchesOneOf(token, "set-info");
+  }
+
   /**
    * Check if the token is a function or variable declaration.
    *