Fix parsing for Princess and make sure that an IllegalArgumentException is thrown if an invalid symbol name is used in the input script

Author: daniel-raffler

src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java

@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.solvers.princess;
 
+import static com.google.common.base.Preconditions.checkArgument;
 import static scala.collection.JavaConverters.asJava;
 import static scala.collection.JavaConverters.collectionAsScalaIterableConverter;
 
@@ -82,6 +83,7 @@
 import org.sosy_lab.common.io.PathCounterTemplate;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 import ostrich.OFlags;
 import ostrich.OstrichStringTheory;
 import scala.Tuple2;
@@ -323,6 +325,17 @@ public List<? extends IExpression> parseStringToTerms(String s, PrincessFormulaC
 
     final List<IFormula> formulas = asJava(parserResult._1());
 
+    // Check that all user defined function, constant and predicate symbols have valid names
+    for (IFunction f : asJava(parserResult._2().keys())) {
+      checkArgument(FormulaCreator.isValidName(FormulaCreator.dequote(f.name())));
+    }
+    for (ConstantTerm c : asJava(parserResult._3().keys())) {
+      checkArgument(FormulaCreator.isValidName(FormulaCreator.dequote(c.name())));
+    }
+    for (Predicate p : asJava(parserResult._4().keys())) {
+      checkArgument(FormulaCreator.isValidName(FormulaCreator.dequote(p.name())));
+    }
+
     ImmutableSet.Builder<IExpression> declaredFunctions = ImmutableSet.builder();
     for (IExpression f : formulas) {
       declaredFunctions.addAll(creator.extractVariablesAndUFs(f, true).values());