From 58c6c715b00693bc3e385a991e05e45a58fca3f0 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                 |  8 +++-----
 silicon.sh                  | 10 ++++------
 src/main/scala/Config.scala | 11 +++++------
 3 files changed, 12 insertions(+), 17 deletions(-)

diff --git a/silicon.bat b/silicon.bat
index b618f508b..d352211fc 100644
--- a/silicon.bat
+++ b/silicon.bat
@@ -4,7 +4,7 @@ set CURR_DIR=%cd%
 set BASE_DIR=%~dp0
 
 :: switch to repository root to check for classpath file and possibly call sbt.
-cd %BASE_DIR%
+cd "%BASE_DIR%"
 
 :: Only call sbt if the classpath file is missing.
 if not exist silicon_classpath.txt (
@@ -22,12 +22,10 @@ if not exist silicon_classpath.txt (
 for /f "delims=" %%x in (silicon_classpath.txt) do set CP=%%x
 
 :: switch back to original directory
-cd %CURR_DIR%
+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..4df028979 100755
--- a/silicon.sh
+++ b/silicon.sh
@@ -4,14 +4,12 @@
 
 set -e
 
-set -e
-
-BASEDIR="$(realpath `dirname $0`)"
+BASEDIR="$(realpath "$(dirname "$0")")"
 
 CP_FILE="$BASEDIR/silicon_classpath.txt"
 
-if [ ! -f $CP_FILE ]; then
-    (cd $BASEDIR; sbt "export runtime:dependencyClasspath" | tail -n1 > $CP_FILE)
+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