From 0ce174701adfdbd7e083ee05aad1b8a18deea137 Mon Sep 17 00:00:00 2001
From: Federico Poli <federpoli@gmail.com>
Date: Wed, 19 Jan 2022 10:32:03 +0100
Subject: [PATCH] Remove quotes around Z3 arguments

---
 silicon.bat                 |  4 +---
 silicon.sh                  |  4 +---
 src/main/scala/Config.scala | 11 +++++------
 3 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/silicon.bat b/silicon.bat
index b618f508b..3d51d3a62 100644
--- a/silicon.bat
+++ b/silicon.bat
@@ -27,7 +27,5 @@ cd %CURR_DIR%
 set JAVA_EXE=java
 set JVM_OPTS=-Dlogback.configurationFile="%BASE_DIR%\src\main\resources\logback.xml" -Xss16m -Dfile.encoding=UTF-8
 set SILICON_MAIN=viper.silicon.SiliconRunner
-set FWD_ARGS= %*
-set CMD=%JAVA_EXE% %JVM_OPTS% -cp "%CP%" %SILICON_MAIN% %FWD_ARGS%
 
-call %CMD%
+call %JAVA_EXE% %JVM_OPTS% -cp "%CP%" %SILICON_MAIN% %*
diff --git a/silicon.sh b/silicon.sh
index c5dd3c38a..72b84f87a 100755
--- a/silicon.sh
+++ b/silicon.sh
@@ -4,8 +4,6 @@
 
 set -e
 
-set -e
-
 BASEDIR="$(realpath `dirname $0`)"
 
 CP_FILE="$BASEDIR/silicon_classpath.txt"
@@ -14,4 +12,4 @@ if [ ! -f $CP_FILE ]; then
     (cd $BASEDIR; sbt "export runtime:dependencyClasspath" | tail -n1 > $CP_FILE)
 fi
 
-java -Xss30M -Dlogback.configurationFile="$BASEDIR/src/main/resources/logback.xml" -cp "`cat $CP_FILE`" viper.silicon.SiliconRunner $@
+exec java -Xss30M -Dlogback.configurationFile="$BASEDIR/src/main/resources/logback.xml" -cp "`cat $CP_FILE`" viper.silicon.SiliconRunner "$@"
diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index a2d7f94ea..4c558af52 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -54,10 +54,9 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   private val smtlibOptionsConverter: ValueConverter[Map[String, String]] = new ValueConverter[Map[String, String]] {
     def parse(s: List[(String, List[String])]): Either[String, Option[Map[String, String]]] = s match {
-      case (_, str :: Nil) :: Nil if str.head == '"' && str.last == '"' =>
+      case (_, str :: Nil) :: Nil =>
         val config = toMap(
-          str.substring(1, str.length - 1) /* Drop leading and trailing quotation mark */
-             .split(' ') /* Separate individual key=value pairs */
+          str.split(' ') /* Separate individual key=value pairs */
              .map(_.trim)
              .filter(_.nonEmpty)
              .map(_.split('=')) /* Split key=value pairs */
@@ -367,15 +366,15 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val z3Args: ScallopOption[String] = opt[String]("z3Args",
     descr = (  "Command-line arguments which should be forwarded to Z3. "
-             + "The expected format is \"<opt> <opt> ... <opt>\", including the quotation marks."),
+             + "The expected format is \"<opt> <opt> ... <opt>\", excluding the quotation marks."),
     default = None,
     noshort = true
-  )(forwardArgumentsConverter)
+  )
 
   val z3ConfigArgs: ScallopOption[Map[String, String]] = opt[Map[String, String]]("z3ConfigArgs",
     descr = (  "Configuration options which should be forwarded to Z3. "
              + "The expected format is \"<key>=<val> <key>=<val> ... <key>=<val>\", "
-             + "including the quotation marks. "
+             + "excluding the quotation marks. "
              + "The configuration options given here will override those from Silicon's Z3 preamble."),
     default = Some(Map()),
     noshort = true