From 7aa97f1879aa5bc7a43bc35b2c92a9124530023d Mon Sep 17 00:00:00 2001
From: Federico Poli <federpoli@gmail.com>
Date: Tue, 18 Jan 2022 18:08:28 +0100
Subject: [PATCH] Report quantifier instantiations

---
 silicon.sh                                 | 10 ++++------
 src/main/scala/decider/Z3ProverStdIO.scala | 10 +++++++++-
 2 files changed, 13 insertions(+), 7 deletions(-)

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/decider/Z3ProverStdIO.scala b/src/main/scala/decider/Z3ProverStdIO.scala
index c8a08718c..a249891bb 100644
--- a/src/main/scala/decider/Z3ProverStdIO.scala
+++ b/src/main/scala/decider/Z3ProverStdIO.scala
@@ -425,7 +425,15 @@ class Z3ProverStdIO(uniqueId: String,
         logger warn msg
       }
 
-      repeat = warning
+      // When `smt.qi.profile` is `true`, Z3 periodically reports the quantifier instantiations using the format
+      // `[quantifier_instances] "<quantifier_id>" : <instances> : <maximum generation> : <maximum cost>`.
+      // See: https://github.com/Z3Prover/z3/issues/4522
+      val qiProfile = result.startsWith("[quantifier_instances]")
+      if (qiProfile) {
+        logger info result
+      }
+
+      repeat = warning || qiProfile
     }
 
     result