Experimental proverArgs annotation for methods

src/main/scala/decider/ProverStdIO.scala

@@ -195,6 +195,15 @@ abstract class ProverStdIO(uniqueId: String,
     readSuccess()
   }
 
+  override def setOption(name: String, value: String): String = {
+    writeLine(s"(get-option :${name})")
+    val oldVal = readLine()
+    if (oldVal == "unsupported")
+      throw ProverInteractionFailed(uniqueId, s"Prover does not support option $name")
+    emit(s"(set-option :$name $value)")
+    oldVal
+  }
+
 //  private val quantificationLogger = bookkeeper.logfiles("quantification-problems")
 
   def assume(term: Term): Unit = {

src/main/scala/decider/Z3ProverAPI.scala

@@ -20,7 +20,7 @@ import java.nio.file.Path
 import scala.collection.mutable
 import com.microsoft.z3._
 import com.microsoft.z3.enumerations.Z3_param_kind
-import viper.silicon.reporting.ExternalToolError
+import viper.silicon.reporting.{ExternalToolError, ProverInteractionFailed}
 
 import scala.jdk.CollectionConverters.MapHasAsJava
 import scala.util.Random
@@ -236,6 +236,10 @@ class Z3ProverAPI(uniqueId: String,
     }
   }
 
+  override def setOption(name: String, value: String): String = {
+    throw new ProverInteractionFailed(uniqueId, "Dynamically setting prover options via Z3 API is currently not supported.")
+  }
+
   def assume(term: Term): Unit = {
     try {
       if (preamblePhaseOver)

src/main/scala/interfaces/decider/Prover.scala

@@ -22,6 +22,7 @@ trait ProverLike {
   def emit(content: String): Unit
   def emit(contents: Iterable[String]): Unit = { contents foreach emit }
   def emitSettings(contents: Iterable[String]): Unit
+  def setOption(name: String, value: String): String
   def assume(term: Term): Unit
   def declare(decl: Decl): Unit
   def comment(content: String): Unit

src/main/scala/supporters/MethodSupporter.scala

@@ -18,6 +18,7 @@ import viper.silicon.state.{Heap, State, Store}
 import viper.silicon.state.State.OldHeaps
 import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silicon.utils.freshSnap
+import viper.silver.reporter.AnnotationWarning
 
 /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */
 
@@ -44,6 +45,23 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
       logger.debug("\n\n" + "-" * 10 + " METHOD " + method.name + "-" * 10 + "\n")
       decider.prover.comment("%s %s %s".format("-" * 10, method.name, "-" * 10))
 
+      val toReset = method.info.getUniqueInfo[ast.AnnotationInfo] match {
+        case Some(ai) if ai.values.contains("proverArgs") =>
+          ai.values("proverArgs").flatMap(o => {
+            val index = o.indexOf("=")
+            if (index == -1) {
+              reporter report AnnotationWarning(s"Invalid proverArgs annotation ${o} on method ${method.name}. Required format for each option is optionName=value.")
+              None
+            } else {
+              val (name, value) = (o.take(index), o.drop(index + 1))
+              val oldVal = v.decider.prover.setOption(name, value)
+              Some((name, oldVal))
+            }
+          })
+        case _ =>
+          Seq()
+      }
+
       openSymbExLogger(method)
 
       val pres = method.pres
@@ -94,6 +112,8 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
                     consumes(s4, posts, postViolated, v4)((_, _, _) =>
                       Success()))}) }  )})})
 
+      toReset.foreach(o => v.decider.prover.setOption(o._1, o._2))
+
       symbExLog.closeMemberScope()
       Seq(result)
     }

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -150,6 +150,11 @@ class DefaultMainVerifier(config: Config,
       decider.prover.emitSettings(contents)
       _verificationPoolManager.pooledVerifiers.emitSettings(contents)
     }
+
+    override def setOption(name: String, value: String): String = {
+      decider.prover.setOption(name, value)
+      _verificationPoolManager.pooledVerifiers.setOption(name, value)
+    }
   }
 
   /* Program verification */

src/main/scala/verifier/VerificationPoolManager.scala

@@ -37,6 +37,9 @@ class VerificationPoolManager(mainVerifier: MainVerifier) extends StatefulCompon
 
     override def emitSettings(contents: Iterable[String]): Unit =
       workerVerifiers foreach (_.decider.prover.emitSettings(contents))
+
+    override def setOption(name: String, value: String): String =
+      (workerVerifiers map (_.decider.prover.setOption(name, value))).head
   }
 
   /* Verifier pool management */