diff --git a/build.sbt b/build.sbt
index 8be65979d..8ba98c800 100644
--- a/build.sbt
+++ b/build.sbt
@@ -30,6 +30,7 @@ lazy val silicon = (project in file("."))
     libraryDependencies += "com.typesafe.scala-logging" %% "scala-logging" % "3.9.2",
     libraryDependencies += "org.apache.commons" % "commons-pool2" % "2.9.0",
     libraryDependencies += "io.spray" %%  "spray-json" % "1.3.6",
+    libraryDependencies += "com.microsoft.z3" % "z3" % "4.8.7" from "https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/com.microsoft.z3-4.8.7.jar",
 
     // Only get a few compilation errors at once
     maxErrors := 5,
diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 2320b4531..6159767ae 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -12,7 +12,7 @@ import scala.util.matching.Regex
 import scala.util.Properties._
 import org.rogach.scallop._
 import viper.silicon.Config.StateConsolidationMode.StateConsolidationMode
-import viper.silicon.decider.{Z3ProverStdIO, Cvc5ProverStdIO}
+import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverAPI, Z3ProverStdIO}
 import viper.silver.frontend.SilFrontendConfig
 
 class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
@@ -635,6 +635,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val parallelizeBranches= opt[Boolean]("parallelizeBranches",
+    descr = "Verify different branches in parallel.",
+    default = Some(false),
+    noshort = true
+  )
+
   val printTranslatedProgram: ScallopOption[Boolean] = opt[Boolean]("printTranslatedProgram",
     descr ="Print the final program that is going to be verified to stdout.",
     default = Some(false),
@@ -717,7 +723,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   )
 
   val prover: ScallopOption[String] = opt[String]("prover",
-    descr = s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}. " +
+    descr = s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}, ${Z3ProverAPI.name}. " +
             s"(default: ${Z3ProverStdIO.name}).",
     default = Some(Z3ProverStdIO.name),
     noshort = true
@@ -726,8 +732,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {
-    case Some(Z3ProverStdIO.name) | Some(Cvc5ProverStdIO.name) => Right(())
-    case prover => Left(s"Unknown prover '$prover' provided. Expected one of ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}.")
+    case Some(Z3ProverStdIO.name) | Some(Cvc5ProverStdIO.name) | Some(Z3ProverAPI.name) => Right(())
+    case prover => Left(s"Unknown prover '$prover' provided. Expected one of ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}, ${Z3ProverAPI.name}.")
   }
 
   validateOpt(timeout) {
diff --git a/src/main/scala/decider/CVC5ProverStdIO.scala b/src/main/scala/decider/CVC5ProverStdIO.scala
index 65ee2db52..cece2a4e0 100644
--- a/src/main/scala/decider/CVC5ProverStdIO.scala
+++ b/src/main/scala/decider/CVC5ProverStdIO.scala
@@ -45,4 +45,6 @@ class Cvc5ProverStdIO(uniqueId: String,
   protected def getProverPath: Path = {
     Paths.get(Verifier.config.cvc5Exe)
   }
+
+  override def emitSettings(contents: Iterable[String]): Unit = emit(contents)
 }
diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index cdc187d96..5309f903e 100644
--- a/src/main/scala/decider/Decider.scala
+++ b/src/main/scala/decider/Decider.scala
@@ -10,11 +10,11 @@ import scala.reflect.{ClassTag, classTag}
 import com.typesafe.scalalogging.Logger
 import viper.silver.ast
 import viper.silver.components.StatefulComponent
-import viper.silver.verifier.DependencyNotFoundError
+import viper.silver.verifier.{DependencyNotFoundError, Model}
 import viper.silicon._
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces._
-import viper.silicon.interfaces.decider.{Prover, Unsat}
+import viper.silicon.interfaces.decider._
 import viper.silicon.logger.SymbExLogger
 import viper.silicon.logger.records.data.{DeciderAssertRecord, DeciderAssumeRecord, ProverAssertRecord}
 import viper.silicon.state._
@@ -60,15 +60,17 @@ trait Decider {
   def appliedFresh(id: String, sort: Sort, appliedArgs: Seq[Term]): App
 
   def generateModel(): Unit
-  def getModel(): String
+  def getModel(): Model
   def clearModel(): Unit
+  def hasModel(): Boolean
+  def isModelValid(): Boolean
 
 /* [BRANCH-PARALLELISATION] */
-//  def freshFunctions: InsertionOrderedSet[FunctionDecl]
-//  def freshMacros: Vector[MacroDecl]
-//  def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit
-//  def declareAndRecordAsFreshMacros(functions: Vector[MacroDecl]): Unit
-//  def setPcs(other: PathConditionStack): Unit
+  def freshFunctions: InsertionOrderedSet[FunctionDecl]
+  def freshMacros: Vector[MacroDecl]
+  def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit
+  def declareAndRecordAsFreshMacros(functions: Vector[MacroDecl]): Unit
+  def setPcs(other: PathConditionStack): Unit
 
   def statistics(): Map[String, String]
 }
@@ -87,49 +89,64 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
   def identifierFactory: IdentifierFactory
 
   object decider extends Decider with StatefulComponent {
-    private var proverStdIO: ProverStdIO = _
+    private var _prover: Prover = _
     private var pathConditions: PathConditionStack = _
 
-//    private var _freshFunctions: InsertionOrderedSet[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
-//    private var _freshMacros: Vector[MacroDecl] = _
+    private var _freshFunctions: InsertionOrderedSet[FunctionDecl] = _ /* [BRANCH-PARALLELISATION] */
+    private var _freshMacros: Vector[MacroDecl] = _
 
-    def prover: ProverStdIO = proverStdIO
+    def prover: Prover = _prover
 
     def pcs: PathConditionStack = pathConditions
 
-//    def setPcs(other: PathConditionStack) = { /* [BRANCH-PARALLELISATION] */
-//      pathConditions = other
-//      pathConditions.assumptions foreach prover.assume
-//    }
-    private def getProverStdIO(prover: String): ProverStdIO = prover match {
+    def setPcs(other: PathConditionStack) = {
+      /* [BRANCH-PARALLELISATION] */
+      pathConditions = other
+      while (prover.pushPopScopeDepth > 1){
+        prover.pop()
+      }
+      // TODO: Change interface to make the cast unnecessary?
+      val layeredStack = other.asInstanceOf[LayeredPathConditionStack]
+      layeredStack.layers.reverse.foreach(l => {
+        l.assumptions foreach prover.assume
+        prover.push()
+      })
+    }
+
+    private def getProver(prover: String): Prover = prover match {
       case Z3ProverStdIO.name => new Z3ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
       case Cvc5ProverStdIO.name => new Cvc5ProverStdIO(uniqueId, termConverter, identifierFactory, reporter)
+      case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter)
       case prover =>
         val msg1 = s"Unknown prover '$prover' provided. Defaulting to ${Z3ProverStdIO.name}."
         logger warn msg1
-        getProverStdIO(Z3ProverStdIO.name)
+        getProver(Z3ProverStdIO.name)
     }
 
     private def createProver(): Option[DependencyNotFoundError] = {
-      proverStdIO = getProverStdIO(Verifier.config.prover())
+      _prover = getProver(Verifier.config.prover())
 
-      proverStdIO.start() /* Cannot query prover version otherwise */
+      _prover.start() /* Cannot query prover version otherwise */
 
-      val proverStdIOVersion = proverStdIO.version()
+      val proverVersion = _prover.version()
       // One can pass some options. This allows to check whether they have been received.
 
-      val msg = s"Using ${proverStdIO.name} $proverStdIOVersion located at ${proverStdIO.proverPath}"
+      val path = prover match {
+        case pio: ProverStdIO => pio.proverPath
+        case _ => "No Path"
+      }
+      val msg = s"Using ${_prover.name} $proverVersion located at ${path}"
       reporter report ConfigurationConfirmation(msg)
       logger debug msg
 
-      if (proverStdIOVersion < proverStdIO.minVersion) {
-        val msg1 = s"Expected at least ${proverStdIO.name} version ${proverStdIO.minVersion.version}, but found $proverStdIOVersion"
+      if (proverVersion < _prover.minVersion) {
+        val msg1 = s"Expected at least ${_prover.name} version ${_prover.minVersion.version}, but found $proverVersion"
         reporter report InternalWarningMessage(msg1)
         logger warn msg1
       }
 
-      if (proverStdIO.maxVersion.fold(false)(_ < proverStdIOVersion)) {
-        val msg1 = s"Silicon might not work with ${proverStdIO.name} version $proverStdIOVersion, consider using ${proverStdIO.maxVersion.get}"
+      if (_prover.maxVersion.fold(false)(_ < proverVersion)) {
+        val msg1 = s"Silicon might not work with ${_prover.name} version $proverVersion, consider using ${_prover.maxVersion.get}"
         reporter report InternalWarningMessage(msg1)
         logger warn msg1
       }
@@ -141,20 +158,20 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def start(): Unit = {
       pathConditions = new LayeredPathConditionStack()
-//      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
-//      _freshMacros = Vector.empty
+      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
+      _freshMacros = Vector.empty
       createProver()
     }
 
     def reset(): Unit = {
-      proverStdIO.reset()
+      _prover.reset()
       pathConditions = new LayeredPathConditionStack()
-//      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
-//      _freshMacros = Vector.empty
+      _freshFunctions = InsertionOrderedSet.empty /* [BRANCH-PARALLELISATION] */
+      _freshMacros = Vector.empty
     }
 
     def stop(): Unit = {
-      if (proverStdIO != null) proverStdIO.stop()
+      if (_prover != null) _prover.stop()
     }
 
     /* Assumption scope handling */
@@ -163,14 +180,14 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       //val commentRecord = new CommentRecord("push", null, null)
       //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord)
       pathConditions.pushScope()
-      proverStdIO.push()
+      _prover.push()
       //SymbExLogger.currentLog().closeScope(sepIdentifier)
     }
 
     def popScope(): Unit = {
       //val commentRecord = new CommentRecord("pop", null, null)
       //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord)
-      proverStdIO.pop()
+      _prover.pop()
       pathConditions.popScope()
       //SymbExLogger.currentLog().closeScope(sepIdentifier)
     }
@@ -298,7 +315,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
       prover.declare(macroDecl)
 
-//      _freshMacros = _freshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
+      _freshMacros = _freshMacros :+ macroDecl /* [BRANCH-PARALLELISATION] */
 
       macroDecl
     }
@@ -334,27 +351,27 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
               HeapDepFun(proverFun.id, proverFun.argSorts, proverFun.resultSort).asInstanceOf[F]
           }
 
-//      _freshFunctions = _freshFunctions + FunctionDecl(fun) /* [BRANCH-PARALLELISATION] */
+      _freshFunctions = _freshFunctions + FunctionDecl(fun) /* [BRANCH-PARALLELISATION] */
 
       fun
     }
 
 
 /* [BRANCH-PARALLELISATION] */
-//    def freshFunctions: InsertionOrderedSet[FunctionDecl] = _freshFunctions
-//    def freshMacros: Vector[MacroDecl] = _freshMacros
-//
-//    def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit = {
-//      functions foreach prover.declare
-//
-//      _freshFunctions = _freshFunctions ++ functions
-//    }
-//
-//    def declareAndRecordAsFreshMacros(macros: Vector[MacroDecl]): Unit = {
-//      macros foreach prover.declare
-//
-//      _freshMacros = _freshMacros ++ macros
-//    }
+    def freshFunctions: InsertionOrderedSet[FunctionDecl] = _freshFunctions
+    def freshMacros: Vector[MacroDecl] = _freshMacros
+
+    def declareAndRecordAsFreshFunctions(functions: InsertionOrderedSet[FunctionDecl]): Unit = {
+      functions foreach prover.declare
+
+      _freshFunctions = _freshFunctions ++ functions
+    }
+
+    def declareAndRecordAsFreshMacros(macros: Vector[MacroDecl]): Unit = {
+      macros foreach prover.declare
+
+      _freshMacros = _freshMacros ++ macros
+    }
 
     /* Misc */
 
@@ -362,7 +379,11 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     override def generateModel(): Unit = proverAssert(False(), None)
 
-    override def getModel(): String = prover.getLastModel()
+    override def getModel(): Model = prover.getModel()
+
+    override def hasModel(): Boolean = prover.hasModel()
+
+    override def isModelValid(): Boolean = prover.isModelValid()
 
     override def clearModel(): Unit = prover.clearLastModel()
   }
diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index af0cd74f4..4c2977bb9 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -221,7 +221,7 @@ private[decider] class LayeredPathConditionStack
        with PathConditionStack
        with Cloneable {
 
-  private var layers: Stack[PathConditionStackLayer] = Stack.empty
+  /* private */ var layers: Stack[PathConditionStackLayer] = Stack.empty
   private var markToLength: Map[Mark, Int] = Map.empty
   private var scopeMarks: List[Mark] = List.empty
   private var markCounter = new Counter(0)
diff --git a/src/main/scala/decider/ProverStdIO.scala b/src/main/scala/decider/ProverStdIO.scala
index 4d010f678..5256ed09d 100644
--- a/src/main/scala/decider/ProverStdIO.scala
+++ b/src/main/scala/decider/ProverStdIO.scala
@@ -20,6 +20,7 @@ import viper.silicon.verifier.Verifier
 import viper.silver.verifier.{DefaultDependency => SilDefaultDependency}
 import viper.silicon.{Config, Map, toMap}
 import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage, Reporter}
+import viper.silver.verifier.Model
 
 import scala.collection.mutable
 
@@ -30,7 +31,7 @@ abstract class ProverStdIO(uniqueId: String,
     extends Prover
        with LazyLogging {
 
-  protected var pushPopScopeDepth = 0
+  /* protected */ var pushPopScopeDepth = 0
   protected var lastTimeout: Int = -1
   protected var logfileWriter: PrintWriter = _
   protected var prover: Process = _
@@ -41,14 +42,9 @@ abstract class ProverStdIO(uniqueId: String,
   var proverPath: Path = _
   var lastModel : String = _
 
-  def name: String
-  def minVersion: Version
-  def maxVersion: Option[Version]
   def exeEnvironmentalVariable: String
   def dependencies: Seq[SilDefaultDependency]
-  def staticPreamble: String
   def startUpArgs: Seq[String]
-  def randomizeSeedsOptions: Seq[String]
 
   protected def setTimeout(timeout: Option[Int]): Unit
   protected def getProverPath: Path
@@ -289,6 +285,14 @@ abstract class ProverStdIO(uniqueId: String,
     }
   }
 
+  override def hasModel(): Boolean = {
+    lastModel != null
+  }
+
+  override def isModelValid(): Boolean = {
+    lastModel != null && !lastModel.contains("model is not available")
+  }
+
   protected def assertUsingSoftConstraints(goal: String): (Boolean, Long) = {
     val guard = fresh("grd", Nil, sorts.Bool)
 
@@ -457,7 +461,7 @@ abstract class ProverStdIO(uniqueId: String,
     output.println(out)
   }
 
-  override def getLastModel(): String = lastModel
+  override def getModel(): Model = Model(lastModel)
 
   override def clearLastModel(): Unit = lastModel = null
 }
diff --git a/src/main/scala/decider/SMTLib2PreambleReader.scala b/src/main/scala/decider/SMTLib2PreambleReader.scala
index 0d2adb9b4..358b43a45 100644
--- a/src/main/scala/decider/SMTLib2PreambleReader.scala
+++ b/src/main/scala/decider/SMTLib2PreambleReader.scala
@@ -54,8 +54,11 @@ class SMTLib2PreambleReader extends PreambleReader[String, String] {
         lineAcc.replace(orig, repl)})
   }
 
-  def emitPreamble(preamble: Iterable[String], sink: ProverLike): Unit = {
-    sink.emit(preamble)
+  def emitPreamble(preamble: Iterable[String], sink: ProverLike, isOptions: Boolean): Unit = {
+    if (isOptions)
+      sink.emitSettings(preamble)
+    else
+      sink.emit(preamble)
   }
 
   def emitParametricPreamble(resource: String,
@@ -63,6 +66,6 @@ class SMTLib2PreambleReader extends PreambleReader[String, String] {
                              sink: ProverLike)
                             : Unit = {
 
-    emitPreamble(readParametricPreamble(resource, substitutions), sink)
+    emitPreamble(readParametricPreamble(resource, substitutions), sink, false)
   }
 }
diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala
index c8acebb5c..bf62df61e 100644
--- a/src/main/scala/decider/TermToSMTLib2Converter.scala
+++ b/src/main/scala/decider/TermToSMTLib2Converter.scala
@@ -380,7 +380,7 @@ class TermToSMTLib2Converter
     else
       render(t)
 
-  protected def render(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
+  def render(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
     val repr: String = id match {
       case SimpleIdentifier(name) => name
       case SuffixedIdentifier(prefix, separator, suffix) => s"${render(prefix, false)}$separator$suffix"
diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala
new file mode 100644
index 000000000..80ccd6d21
--- /dev/null
+++ b/src/main/scala/decider/TermToZ3APIConverter.scala
@@ -0,0 +1,527 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2019 ETH Zurich.
+
+package viper.silicon.decider
+
+import viper.silicon.decider.SmtlibNameSanitizer
+import viper.silicon.interfaces.decider.TermConverter
+import viper.silicon.state.terms._
+import viper.silicon.state.{Identifier, SimpleIdentifier, SortBasedIdentifier, SuffixedIdentifier}
+import viper.silver.components.StatefulComponent
+import com.microsoft.z3.{ArithExpr, BoolExpr, Context, DatatypeSort, IntExpr, RealExpr, Expr => Z3Expr, FuncDecl => Z3FuncDecl, Sort => Z3Sort, Symbol => Z3Symbol}
+
+import scala.collection.mutable
+
+class TermToZ3APIConverter
+    extends TermConverter[Z3Expr, Z3Sort, Unit]
+       with StatefulComponent {
+
+  private var sanitizedNamesCache: mutable.Map[String, String] = _
+
+  private val nameSanitizer = new SmtlibNameSanitizer
+
+  private val smtlibConverter = new TermToSMTLib2Converter()
+
+  var ctx: Context = _
+  val macros = mutable.HashMap[String, (Seq[Var], Term)]()
+
+  val sortCache = mutable.HashMap[Sort, Z3Sort]()
+  val funcDeclCache = mutable.HashMap[(String, Seq[Sort], Sort), Z3FuncDecl]()
+
+  def convert(s: Sort): Z3Sort = convertSort(s)
+
+  def convertId(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
+    smtlibConverter.render(id, sanitizeIdentifier)
+  }
+
+  def getSnapSort = {
+    if (snapSort == null) {
+      /*
+      (declare-datatypes (($Snap 0)) ((
+      ($Snap.unit)
+      ($Snap.combine ($Snap.first $Snap) ($Snap.second $Snap)))))
+     */
+      val unit = ctx.mkConstructor("$Snap.unit", "is_$Snap.unit", null, null, null)
+
+      val sortArray: Array[Z3Sort] = Array(null, null)
+      val combine = ctx.mkConstructor("$Snap.combine", "is_$Snap.combine", Array("$Snap.first", "$Snap.second"), sortArray, Array(0, 0))
+      snapSort = ctx.mkDatatypeSort("$Snap", Array(unit, combine))
+      unitConstructor = unit.ConstructorDecl()
+      combineConstructor = combine.ConstructorDecl()
+      val accessors = combine.getAccessorDecls
+      firstFunc = accessors(0)
+      secondFunc = accessors(1)
+    }
+    snapSort
+  }
+  def getUnitConstructor = {
+    if (unitConstructor == null)
+      getSnapSort
+    unitConstructor
+  }
+
+  def getCombineConstructor = {
+    if (combineConstructor == null)
+      getSnapSort
+    combineConstructor
+  }
+
+  def getFirstFunc = {
+    if (firstFunc == null)
+      getSnapSort
+    firstFunc
+  }
+
+  def getSecondFunc = {
+    if (secondFunc == null)
+      getSnapSort
+    secondFunc
+  }
+
+  var snapSort : DatatypeSort = _
+  var unitConstructor : Z3FuncDecl = _
+  var combineConstructor: Z3FuncDecl = _
+  var firstFunc: Z3FuncDecl = _
+  var secondFunc: Z3FuncDecl = _
+
+  def convertSort(s: Sort): Z3Sort = {
+    val existingEntry = sortCache.get(s)
+    if (existingEntry.isDefined)
+      return existingEntry.get
+    val res = s match {
+      case sorts.Int => ctx.mkIntSort()
+      case sorts.Bool => ctx.mkBoolSort()
+      case sorts.Perm => ctx.mkRealSort()
+      case sorts.Snap => getSnapSort
+      case sorts.Ref => ctx.mkUninterpretedSort("$Ref")
+      case sorts.Map(keySort, valueSort) => ctx.mkUninterpretedSort("Map<" + convertSortName(keySort) + "~_" + convertSortName(valueSort) + ">")
+      case sorts.Seq(elementSort) => {
+        val res = ctx.mkUninterpretedSort("Seq<" + convertSortName(elementSort) + ">")
+        res
+      }
+      case sorts.Set(elementSort) => ctx.mkUninterpretedSort("Set<" + convertSortName(elementSort) + ">")
+      case sorts.Multiset(elementSort) => ctx.mkUninterpretedSort("Multiset<" + convertSortName(elementSort) + ">")
+      case sorts.UserSort(id) => ctx.mkUninterpretedSort(convertId(id))
+      case sorts.SMTSort(id) => {
+        // workaround: since we cannot create a built-in sort from its name, we let Z3 parse
+        // a string that uses the sort, take the AST, and get the func decl from there, so that we can
+        // programmatically create a func app.
+        val workaround = ctx.parseSMTLIB2String(s"(declare-const workaround ${id}) (assert (= workaround workaround))", null, null, null, null)
+        val res = workaround(0).getArgs()(0).getSort
+        res
+      }
+
+      case sorts.Unit =>
+        /* Should never occur
+         */
+        ???
+
+      case sorts.FieldValueFunction(codomainSort) => {
+        val name = convertSortName(codomainSort)
+        ctx.mkUninterpretedSort("$FVF<" + name + ">")
+      }
+      case sorts.PredicateSnapFunction(codomainSort) => ctx.mkUninterpretedSort("$PSF<" + convertSortName(codomainSort) + ">")
+
+      case sorts.FieldPermFunction() => ctx.mkUninterpretedSort("$FPM") // text("$FPM")
+      case sorts.PredicatePermFunction() => ctx.mkUninterpretedSort("$PPM") // text("$PPM")
+    }
+    sortCache.update(s, res)
+    res
+  }
+
+  def convertSortSymbol(s: Sort): Option[Z3Symbol] = {
+    s match {
+      case sorts.Int => None
+      case sorts.Bool => None
+      case sorts.Perm => None
+      case sorts.Snap => Some(ctx.mkSymbol("$Snap"))
+      case sorts.Ref => Some(ctx.mkSymbol("$Ref"))
+      case sorts.Map(keySort, valueSort) => Some(ctx.mkSymbol("Map<" + convertSortName(keySort) + "~_" + convertSortName(valueSort) + ">"))
+      case sorts.Seq(elementSort) => Some(ctx.mkSymbol("Seq<" + convertSortName(elementSort) + ">"))
+      case sorts.Set(elementSort) => Some(ctx.mkSymbol("Set<" + convertSortName(elementSort) + ">"))
+      case sorts.Multiset(elementSort) => Some(ctx.mkSymbol("Multiset<" + convertSortName(elementSort) + ">"))
+      case sorts.UserSort(id) => Some(ctx.mkSymbol(convertId(id)))
+      case sorts.SMTSort(_) => {
+        ???
+      }
+
+      case sorts.Unit =>
+        /* Should never occur
+         */
+        ???
+
+      case sorts.FieldValueFunction(codomainSort) => Some(ctx.mkSymbol("$FVF<" + convertSortName(codomainSort) + ">")) //
+      case sorts.PredicateSnapFunction(codomainSort) => Some(ctx.mkSymbol("$PSF<" + convertSortName(codomainSort) + ">"))
+
+      case sorts.FieldPermFunction() => Some(ctx.mkSymbol("$FPM")) // text("$FPM")
+      case sorts.PredicatePermFunction() => Some(ctx.mkSymbol("$PPM")) // text("$PPM")
+    }
+  }
+
+  def convertSortName(sort: Sort): String = {
+    smtlibConverter.convertSanitized(sort)
+  }
+
+  def convert(fd: FunctionDecl): Z3FuncDecl = {
+    ctx.mkFuncDecl(convertId(fd.func.id), fd.func.argSorts.filter(s => s != viper.silicon.state.terms.sorts.Unit).map(convertSort(_)).toArray, convertSort(fd.func.resultSort))
+  }
+
+  def convertFuncSymbol(fd: FunctionDecl): Z3Symbol = {
+    ctx.mkSymbol(convertId(fd.func.id))
+  }
+  
+  def convert(md: MacroDecl): (Z3FuncDecl, BoolExpr) = {
+    val func = ctx.mkFuncDecl(convertId(md.id), md.args.map(a => convertSort(a.sort)).toArray, convertSort(md.body.sort))
+    val app = ctx.mkApp(func, md.args.map(convert(_)).toArray : _*)
+    val patterns = Array(ctx.mkPattern(app))
+    val quant = ctx.mkForall(md.args.map(convert(_)).toArray, ctx.mkEq(convertTerm(md.body), app), 1, patterns, null, ctx.mkSymbol(md.id.name), null)
+    (func, quant)
+  }
+
+  def convert(swd: SortWrapperDecl): Z3FuncDecl = {
+    val id = swd.id
+    val fct = FunctionDecl(Fun(id, swd.from, swd.to))
+    convert(fct)
+  }
+
+  def convertSortWrapperSymbol(swd: SortWrapperDecl) = {
+    val id = swd.id
+    val fct = FunctionDecl(Fun(id, swd.from, swd.to))
+    convertFuncSymbol(fct)
+  }
+
+  def convert(d: Decl): Unit = {
+    // not used
+    ???
+  }
+
+  def convert(t: Term): Z3Expr = {
+    convertTerm(t)
+  }
+
+
+  def convertTerm(term: Term): Z3Expr = {
+    val res = term match {
+      case l: Literal => {
+        l match {
+          case IntLiteral(n) => {
+            if (n >= 0)
+              ctx.mkInt(n.toString())
+            else
+              ctx.mkUnaryMinus(ctx.mkInt((-n).toString()))
+          }
+          case True() => ctx.mkTrue()
+          case False() => ctx.mkFalse()
+          case Null() => ctx.mkConst("$Ref.null", ctx.mkUninterpretedSort("$Ref"))
+          case Unit => ctx.mkConst(getUnitConstructor)
+          case _: SeqNil => createApp("Seq_empty", Seq(), l.sort)
+          case _: EmptySet => createApp("Set_empty", Seq(), l.sort)
+          case _: EmptyMultiset => createApp("Multiset_empty", Seq(), l.sort)
+          case _: EmptyMap => createApp("Map_empty", Seq(), l.sort)
+        }
+      }
+
+      case Ite(t0, t1, t2) =>
+        ctx.mkITE(convertTerm(t0).asInstanceOf[BoolExpr], convertTerm(t1), convertTerm(t2))
+
+      case x: Var =>
+        ctx.mkConst(convertId(x.id), convertSort(x.sort))
+
+      case fapp: Application[_] =>
+        fapp.applicable match {
+          case _: SMTFun => createSMTApp(convertId(fapp.applicable.id, false), fapp.args, fapp.sort)
+          case _ => {
+            if (macros.contains(fapp.applicable.id.name)) {
+              val (vars, body) = macros(fapp.applicable.id.name)
+              if (vars.length != fapp.args.length)
+                sys.error("macro usage doesn't match")
+              val substituted = body.replace(vars, fapp.args)
+              val res = convert(substituted)
+              res
+            }else {
+              createApp(convertId(fapp.applicable.id), fapp.args, fapp.sort)
+            }
+          }
+        }
+
+
+      /* Handle quantifiers that have at most one trigger set */
+      case Quantification(quant, vars, body, triggers, name, _) => {
+        if (vars.isEmpty) {
+          convertTerm(body)
+        } else{
+          val qvarExprs = vars.map(v => convert(v)).toArray
+          val nonEmptyTriggers = triggers.filter(_.p.nonEmpty)
+          val patterns = if (nonEmptyTriggers.nonEmpty) nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(convertTerm): _*)).toArray else null
+          if (quant == Forall) {
+            ctx.mkForall(qvarExprs, convertTerm(body), 1, patterns, null, ctx.mkSymbol(name), null)
+          }else{
+            ctx.mkExists(qvarExprs, convertTerm(body), 1, patterns, null, ctx.mkSymbol(name), null)
+          }
+        }
+      }
+
+      /* Booleans */
+
+      case uop: Not => ctx.mkNot(convertTerm(uop.p).asInstanceOf[BoolExpr])
+      case And(ts) => ctx.mkAnd(ts.map(convertTerm(_).asInstanceOf[BoolExpr]): _*)
+      case Or(ts) => ctx.mkOr(ts.map(convertTerm(_).asInstanceOf[BoolExpr]): _*)
+      case bop: Implies => ctx.mkImplies(convertTerm(bop.p0).asInstanceOf[BoolExpr], convertTerm(bop.p1).asInstanceOf[BoolExpr])
+      case bop: Iff =>
+      {
+        val t0 = convertTerm(bop.p0).asInstanceOf[BoolExpr]
+        val t1 = convertTerm(bop.p1).asInstanceOf[BoolExpr]
+        val implication1 = ctx.mkImplies(t0, t1)
+        val implication2 = ctx.mkImplies(t1, t0)
+        ctx.mkAnd(implication1, implication2)
+      }
+      case bop: BuiltinEquals => ctx.mkEq(convertTerm(bop.p0), convertTerm(bop.p1))
+
+      case bop: CustomEquals => bop.p0.sort match {
+        case _: sorts.Seq => createApp("Seq_equal", Seq(bop.p0, bop.p1), bop.sort)
+        case _: sorts.Set => createApp("Set_equal", Seq(bop.p0, bop.p1), bop.sort)
+        case _: sorts.Multiset => createApp("Multiset_equal", Seq(bop.p0, bop.p1), bop.sort)
+        case _: sorts.Map => createApp("Map_equal", Seq(bop.p0, bop.p1), bop.sort)
+        case sort => sys.error(s"Don't know how to translate equality between symbols $sort-typed terms")
+      }
+
+      /* Arithmetic */
+
+      case bop: Minus => ctx.mkSub(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+      case bop: Plus => ctx.mkAdd(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+      case bop: Times => ctx.mkMul(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+      case bop: Div => ctx.mkDiv(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+      case bop: Mod => ctx.mkMod(convertTerm(bop.p0).asInstanceOf[IntExpr], convertTerm(bop.p1).asInstanceOf[IntExpr])
+
+      /* Arithmetic comparisons */
+
+      case bop: Less => ctx.mkLt(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+      case bop: AtMost => ctx.mkLe(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+      case bop: AtLeast => ctx.mkGe(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+      case bop: Greater => ctx.mkGt(convertTerm(bop.p0).asInstanceOf[ArithExpr], convertTerm(bop.p1).asInstanceOf[ArithExpr])
+
+      /* Permissions */
+
+
+      case FullPerm() => ctx.mkReal(1)
+      case NoPerm() => ctx.mkReal(0)
+      case FractionPermLiteral(r) => ctx.mkDiv(convertToReal(IntLiteral(r.numerator)), convertToReal(IntLiteral(r.denominator)))
+      case FractionPerm(n, d) => ctx.mkDiv(convertToReal(n), convertToReal(d))
+      case PermLess(t0, t1) => ctx.mkLt(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
+      case PermAtMost(t0, t1) => ctx.mkLe(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
+      case PermPlus(t0, t1) => ctx.mkAdd(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
+      case PermMinus(t0, t1) => ctx.mkSub(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
+      case PermTimes(t0, t1) => ctx.mkMul(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
+      case IntPermTimes(t0, t1) => ctx.mkMul(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr])
+      case PermIntDiv(t0, t1) => ctx.mkDiv(convertToReal(t0), convertToReal(t1))
+      case PermPermDiv(t0, t1) => ctx.mkDiv(convertToReal(t0), convertToReal(t1))
+      case PermMin(t0, t1) => {
+        /*
+        (define-fun $Perm.min ((p1 $Perm) (p2 $Perm)) Real
+    (ite (<= p1 p2) p1 p2))
+         */
+        val e0 = convert(t0).asInstanceOf[ArithExpr]
+        val e1 = convert(t1).asInstanceOf[ArithExpr]
+        ctx.mkITE(ctx.mkLe(e0, e1), e0, e1)
+      }
+      case IsValidPermVar(v) => {
+        /*
+        (define-fun $Perm.isValidVar ((p $Perm)) Bool
+	        (<= $Perm.No p))
+         */
+        ctx.mkLe(ctx.mkReal(0), convert(v).asInstanceOf[ArithExpr])
+      }
+      case IsReadPermVar(v) => {
+        /*
+        (define-fun $Perm.isReadVar ((p $Perm)) Bool
+         (and ($Perm.isValidVar p)
+         (not (= p $Perm.No))))
+         */
+        ctx.mkLt(ctx.mkReal(0), convert(v).asInstanceOf[ArithExpr]) // simplified
+        //ctx.mkAnd(ctx.mkLe(ctx.mkReal(0), convert(v).asInstanceOf[ArithExpr]),
+        //  ctx.mkNot(ctx.mkEq(convert(v).asInstanceOf[ArithExpr], ctx.mkReal(0))))
+      }
+
+      /* Sequences */
+
+      case SeqRanged(t0, t1) => createApp("Seq_range", Seq(t0, t1), term.sort)
+      case SeqSingleton(t0) => createApp("Seq_singleton", Seq(t0), term.sort)
+      case bop: SeqAppend => createApp("Seq_append", Seq(bop.p0, bop.p1), term.sort)
+      case uop: SeqLength => createApp("Seq_length", Seq(uop.p), term.sort)
+      case bop: SeqAt => createApp("Seq_index", Seq(bop.p0, bop.p1), term.sort)
+      case bop: SeqTake => createApp("Seq_take", Seq(bop.p0, bop.p1), term.sort)
+      case bop: SeqDrop => createApp("Seq_drop", Seq(bop.p0, bop.p1), term.sort)
+      case bop: SeqIn => createApp("Seq_contains", Seq(bop.p0, bop.p1), term.sort)
+      case SeqUpdate(t0, t1, t2) => createApp("Seq_update", Seq(t0, t1, t2), term.sort)
+
+      /* Sets */
+
+      case uop: SingletonSet => createApp("Set_singleton", Seq(uop.p), uop.sort)
+      case bop: SetAdd => createApp("Set_unionone", Seq(bop.p0, bop.p1), bop.sort)
+      case uop: SetCardinality => createApp("Set_card", Seq(uop.p), uop.sort)
+      case bop: SetDifference => createApp("Set_difference", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: SetIntersection => createApp("Set_intersection", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: SetUnion => createApp("Set_union", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: SetIn => createApp("Set_in", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: SetSubset => createApp("Set_subset", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: SetDisjoint => createApp("Set_disjoint", Seq(bop.p0, bop.p1), bop.sort)
+
+      /* Multisets */
+
+      case uop: SingletonMultiset => createApp("Multiset_singleton", Seq(uop.p), uop.sort)
+      case bop: MultisetAdd => createApp("Multiset_unionone", Seq(bop.p0, bop.p1), bop.sort)
+      case uop: MultisetCardinality => createApp("Multiset_card", Seq(uop.p), uop.sort)
+      case bop: MultisetDifference => createApp("Multiset_difference", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: MultisetIntersection => createApp("Multiset_intersection", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: MultisetUnion => createApp("Multiset_union", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: MultisetSubset => createApp("Multiset_subset", Seq(bop.p0, bop.p1), bop.sort)
+      case bop: MultisetCount => createApp("Multiset_count", Seq(bop.p0, bop.p1), bop.sort)
+
+      /* Maps */
+
+      case m: MapCardinality => createApp("Map_card", Seq(m.p), m.sort)
+      case m: MapDomain => createApp("Map_domain", Seq(m.p), m.sort)
+      case m: MapRange => createApp("Map_values", Seq(m.p), m.sort)
+      case m: MapLookup => createApp("Map_apply", Seq(m.p0, m.p1), m.sort)
+      case m: MapUpdate => createApp("Map_update", Seq(m.base, m.key, m.value), m.sort)
+
+      /* Quantified Permissions */
+
+      case Domain(id, fvf) => createApp("$FVF.domain_" + id, Seq(fvf), term.sort)
+
+      case Lookup(field, fvf, at) =>
+        createApp("$FVF.lookup_" + field, Seq(fvf, at), term.sort)
+
+      case FieldTrigger(field, fvf, at) => createApp("$FVF.loc_" + field, (fvf.sort match {
+        case sorts.FieldValueFunction(_) => Seq(Lookup(field, fvf, at), at)
+        case _ => Seq(fvf, at)
+      }), term.sort)
+
+      case PermLookup(field, pm, at) => createApp("$FVF.perm_" + field, Seq(pm, at), term.sort)
+
+      case PredicateDomain(id, psf) => createApp("$PSF.domain_" + id, Seq(psf), term.sort)
+
+      case PredicateLookup(id, psf, args) =>
+        val snap: Term = toSnapTree(args)
+        createApp("$PSF.lookup_" + id, Seq(psf, snap), term.sort)
+
+      case PredicateTrigger(id, psf, args) =>
+        val snap: Term = toSnapTree(args)
+        createApp("$PSF.loc_" + id, Seq(PredicateLookup(id, psf, args), snap), term.sort)
+
+      case PredicatePermLookup(predname, pm, args) =>
+        val snap: Term = toSnapTree(args)
+        createApp("$PSF.perm_" + predname, Seq(pm, snap), term.sort)
+
+      /* Other terms */
+
+      case First(t) => ctx.mkApp(firstFunc, convertTerm(t))
+      case Second(t) => ctx.mkApp(secondFunc, convertTerm(t))
+
+      case bop: Combine =>
+        ctx.mkApp(combineConstructor, convertTerm(bop.p0), convertTerm(bop.p1))
+
+      case SortWrapper(t, to) =>
+        createApp(convertId(SortWrapperId(t.sort, to)), Seq(t), to)
+
+      case Distinct(symbols) =>
+        ctx.mkDistinct(symbols.map(s => ctx.mkConst(convertId(s.id), convertSort(s.resultSort))).toSeq: _*)
+
+      case Let(bindings, body) =>
+        convert(body.replace(bindings))
+
+      case _: MagicWandChunkTerm
+         | _: Quantification =>
+        sys.error(s"Unexpected term $term cannot be translated to SMTLib code")
+    }
+    res
+  }
+
+  @inline
+  protected def createApp(functionName: String, args: Seq[Term], outSort: Sort): Z3Expr = {
+    ctx.mkApp(getFuncDecl(functionName, outSort, args.map(_.sort)), args.map(convertTerm(_)): _*)
+  }
+
+  def getFuncDecl(name: String, resSort: Sort, argSorts: Seq[Sort]): Z3FuncDecl = {
+    val existingEntry = funcDeclCache.get((name, argSorts, resSort))
+    if (existingEntry.isDefined)
+      return existingEntry.get
+    val res = ctx.mkFuncDecl(name, argSorts.map(a => convertSort(a)).toArray, convertSort(resSort))
+    funcDeclCache.update((name, argSorts, resSort), res)
+    res
+  }
+
+
+  @inline
+  protected def createSMTApp(functionName: String, args: Seq[Term], outSort: Sort): Z3Expr = {
+    // workaround: since we cannot create a function application with just the name, we let Z3 parse
+    // a string that uses the function, take the AST, and get the func decl from there, so that we can
+    // programmatically create a func app.
+    val decls = args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ")
+    val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
+    val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))"
+    val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null)
+    val app = workaround(0).getArgs()(0)
+    val decl = app.getFuncDecl
+    val actualArgs =  if (decl.getArity > args.length){
+      // the function name we got wasn't just a function name but also contained a first argument.
+      // this happens with float operations where functionName contains a rounding mode.
+      app.getArgs.toSeq.slice(0, decl.getArity - args.length) ++ args.map(convertTerm(_))
+    }else {
+      args.map(convertTerm(_))
+    }
+    ctx.mkApp(decl, actualArgs.toArray : _*)
+  }
+
+
+  protected def convertToReal(t: Term): RealExpr =
+    if (t.sort == sorts.Int)
+      ctx.mkInt2Real(convertTerm(t).asInstanceOf[IntExpr])
+    else
+      convertTerm(t).asInstanceOf[RealExpr]
+
+  protected def render(id: Identifier, sanitizeIdentifier: Boolean = true): String = {
+    val repr: String = id match {
+      case SimpleIdentifier(name) => name
+      case SuffixedIdentifier(prefix, separator, suffix) => s"${render(prefix, false)}$separator$suffix"
+      case SortBasedIdentifier(template, sorts) => template.format(sorts.map(convert): _*)
+    }
+
+    if (sanitizeIdentifier) sanitize(repr)
+    else repr
+  }
+
+  private def sanitize(str: String): String = {
+    val sanitizedName = sanitizedNamesCache.getOrElseUpdate(str, nameSanitizer.sanitize(str))
+
+    sanitizedName
+  }
+
+  def start(): Unit = {
+    sanitizedNamesCache = mutable.Map.empty
+    smtlibConverter.start()
+  }
+
+  def reset(): Unit = {
+    ctx = null
+    smtlibConverter.reset()
+    sanitizedNamesCache.clear()
+    macros.clear()
+    funcDeclCache.clear()
+    sortCache.clear()
+    unitConstructor = null
+    combineConstructor = null
+    firstFunc = null
+    secondFunc = null
+    snapSort = null
+  }
+
+  def stop(): Unit = {
+    if (sanitizedNamesCache != null) sanitizedNamesCache.clear()
+  }
+
+  override def convertSanitized(s: Sort): Z3Sort = convertSort(s)
+}
diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala
new file mode 100644
index 000000000..753244d57
--- /dev/null
+++ b/src/main/scala/decider/Z3ProverAPI.scala
@@ -0,0 +1,453 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2021 ETH Zurich.
+
+package viper.silicon.decider
+
+import com.typesafe.scalalogging.LazyLogging
+import viper.silicon.common.config.Version
+import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat}
+import viper.silicon.state.IdentifierFactory
+import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Sort, SortDecl, SortWrapperDecl, Term, sorts}
+import viper.silicon.{Config, Map}
+import viper.silicon.verifier.Verifier
+import viper.silver.reporter.{InternalWarningMessage, Reporter}
+import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel}
+import java.io.PrintWriter
+import java.nio.file.Path
+
+import scala.collection.mutable
+import com.microsoft.z3._
+import viper.silicon.reporting.ExternalToolError
+
+import scala.collection.immutable.ListMap
+import scala.jdk.CollectionConverters.MapHasAsJava
+import scala.util.Random
+
+
+object Z3ProverAPI {
+  val name = "Z3-API"
+  val minVersion = Version("4.8.6.0")
+  val maxVersion = Some(Version("4.8.7.0")) /* X.Y.Z if that is the *last supported* version */
+
+  // these are not actually used, but since there is a lot of code that expects command line parameters and a
+  // config file, we just supply this information here (whose contents will then be ignored)
+  val exeEnvironmentalVariable = "Z3_EXE"
+  val dependencies = Seq(SilDefaultDependency("Z3", minVersion.version, "https://github.com/Z3Prover/z3"))
+  val staticPreamble = "/z3config.smt2"
+  val startUpArgs = Seq("-smt2", "-in")
+
+  val randomizeSeedsSetting = "RANDOMIZE_SEEDS"
+
+  // All options taken from z3config.smt2 and split up according to argument type and time when it has to be set.
+  // I removed all options that (no longer?) exist, since those result in errors from Z3.
+  val randomizeSeedsOptions = Seq("random_seed")
+  val initialOptions = Map("auto_config" -> "false", "type_check" -> "true")
+  val boolParams = Map(
+    "smt.delay_units" -> true,
+    "nnf.sk_hack" -> true,
+    "smt.mbqi" -> false,
+    "nlsat.randomize" -> true,
+    "nlsat.shuffle_vars" -> false,
+    "smt.arith.random_initial_value" -> true,
+  )
+  val intParams = Map("smt.restart_strategy" -> 0,
+    "smt.case_split" -> 3,
+    "case_split" -> 3,
+    "smt.delay_units_threshold" -> 16,
+    "smt.qi.max_multi_patterns" -> 1000,
+    "smt.phase_selection" -> 0,
+    "sat.random_seed" -> 0,
+    "nlsat.seed" -> 0,
+    "random_seed" -> 0,
+  )
+  val stringParams = Map(
+    //"smt.qi.cost" -> "(+ weight generation)", // cannot set this for some reason, but this is the default value anyway.
+    "sat.phase" -> "caching"
+  )
+  val doubleParams = Map(
+    "smt.restart_factor" -> 1.5,
+    "smt.qi.eager_threshold" -> 100.0,
+  )
+}
+
+
+class Z3ProverAPI(uniqueId: String,
+                  termConverter: TermToZ3APIConverter,
+                  identifierFactory: IdentifierFactory,
+                  reporter: Reporter)
+    extends Prover
+      with LazyLogging
+{
+
+  /* protected */ var pushPopScopeDepth = 0
+  protected var lastTimeout: Int = -1
+  protected var logfileWriter: PrintWriter = _
+  protected var prover: Solver = _
+  protected var ctx: Context = _
+
+  var proverPath: Path = _
+  var lastModel : Model = _
+
+  var emittedPreambleString = mutable.Queue[String]()
+  var preamblePhaseOver = false
+  var preambleAssumes = mutable.LinkedHashSet[BoolExpr]()
+  val emittedSorts = mutable.LinkedHashSet[com.microsoft.z3.Sort]()
+  val emittedSortSymbols = mutable.LinkedHashSet[Symbol]()
+  val emittedFuncs = mutable.LinkedHashSet[FuncDecl]()
+  val emittedFuncSymbols = mutable.Queue[Symbol]()
+
+  // If true, we do not define macros on the Z3 level, but perform macro expansion ourselves on Silicon Terms.
+  // Otherwise, we define a function on the Z3 level and axiomatize it according to the macro definition.
+  // In terms of performance, I could not measure any substantial difference.
+  val expandMacros = true
+
+
+
+  def version(): Version = {
+    var versString = com.microsoft.z3.Version.getFullVersion
+    if (versString.startsWith("Z3 "))
+      versString = versString.substring(3)
+    Version(versString)
+  }
+
+  def start(): Unit = {
+    pushPopScopeDepth = 0
+    lastTimeout = -1
+    logfileWriter = if (Verifier.config.disableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile)
+    ctx = new Context(Z3ProverAPI.initialOptions.asJava)
+    val params = ctx.mkParams()
+    Z3ProverAPI.boolParams.foreach{
+      case (k, v) => params.add(k, v)
+    }
+    Z3ProverAPI.intParams.foreach{
+      case (k, v) => params.add(k, v)
+    }
+    Z3ProverAPI.doubleParams.foreach{
+      case (k, v) => params.add(k, v)
+    }
+    Z3ProverAPI.stringParams.foreach{
+      case (k, v) => params.add(k, v)
+    }
+    prover = ctx.mkSolver()
+    prover.setParameters(params)
+    termConverter.start()
+    termConverter.ctx = ctx
+    emittedPreambleString.clear()
+    preamblePhaseOver = false
+    emittedFuncs.clear()
+    emittedSorts.clear()
+    emittedFuncSymbols.clear()
+    emittedSortSymbols.clear()
+  }
+
+  def reset(): Unit = {
+    termConverter.reset()
+    stop()
+    start()
+  }
+
+  def stop(): Unit = {
+    emittedPreambleString.clear()
+    preamblePhaseOver = false
+    emittedFuncs.clear()
+    emittedSorts.clear()
+    emittedFuncSymbols.clear()
+    emittedSortSymbols.clear()
+    prover = null
+    lastModel = null
+    if (ctx != null){
+      ctx.close()
+      ctx = null
+    }
+  }
+
+  def push(n: Int = 1): Unit = {
+    endPreamblePhase()
+    pushPopScopeDepth += n
+    if (n == 1) {
+      // the normal case; we handle this without invoking a bunch of higher order functions
+      prover.push()
+    } else {
+      // this might never actually happen
+      (0 until n).foreach(_ => prover.push())
+    }
+  }
+
+  def pop(n: Int = 1): Unit = {
+    endPreamblePhase()
+    prover.pop(n)
+    pushPopScopeDepth -= n
+  }
+
+  def emit(content: String): Unit = {
+    if (preamblePhaseOver) {
+      sys.error("emitting phase over")
+    }
+    emittedPreambleString.append(content)
+  }
+
+  override def emit(contents: Iterable[String]): Unit = {
+    if (preamblePhaseOver) {
+      sys.error("emitting phase over")
+    }
+    emittedPreambleString.appendAll(contents)
+  }
+
+  override def emitSettings(contents: Iterable[String]): Unit = {
+    // we ignore this, don't know any better solution atm.
+    // our settings are defined in this class (see above).
+    // except we check if someone gives us our custom randomization string, in which
+    // case we'll directly set the options to randomize.
+    val optionSetString = s"(set-option :${Z3ProverAPI.randomizeSeedsSetting}"
+    if (contents.exists(s => s.startsWith(optionSetString))) {
+      val params = ctx.mkParams()
+      Z3ProverAPI.randomizeSeedsOptions.foreach(o => params.add(o, Random.nextInt(10000)))
+      prover.setParameters(params)
+    }
+  }
+
+  def assume(term: Term): Unit = {
+    try {
+      if (preamblePhaseOver)
+        prover.add(termConverter.convert(term).asInstanceOf[BoolExpr])
+      else
+        preambleAssumes.add(termConverter.convert(term).asInstanceOf[BoolExpr])
+    } catch {
+      case e: Z3Exception => reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage))
+    }
+  }
+
+  def assert(goal: Term, timeout: Option[Int]): Boolean = {
+    endPreamblePhase()
+    setTimeout(timeout)
+
+    try {
+      val (result, _) = Verifier.config.assertionMode() match {
+        case Config.AssertionMode.SoftConstraints => assertUsingSoftConstraints(goal)
+        case Config.AssertionMode.PushPop => assertUsingPushPop(goal)
+      }
+      result
+    } catch {
+      case e: Z3Exception => throw ExternalToolError("Prover", "Z3 error: " + e.getMessage)
+    }
+  }
+
+  protected def assertUsingPushPop(goal: Term): (Boolean, Long) = {
+    endPreamblePhase()
+    push()
+
+    val negatedGoal = ctx.mkNot(termConverter.convert(goal).asInstanceOf[BoolExpr])
+    prover.add(negatedGoal)
+    val startTime = System.currentTimeMillis()
+    val res = prover.check()
+    val endTime = System.currentTimeMillis()
+    val result = res == Status.UNSATISFIABLE
+    pop()
+
+    if (!result) {
+      retrieveAndSaveModel()
+    }
+
+    (result, endTime - startTime)
+  }
+
+  def saturate(data: Option[Config.ProverStateSaturationTimeout]): Unit = {
+    endPreamblePhase()
+    data match {
+      case Some(Config.ProverStateSaturationTimeout(timeout, comment)) => saturate(timeout, comment)
+      case None => /* Don't do anything */
+    }
+  }
+
+  def saturate(timeout: Int, comment: String): Unit = {
+    endPreamblePhase()
+    setTimeout(Some(timeout))
+    prover.check()
+  }
+
+  protected def retrieveAndSaveModel(): Unit = {
+    if (Verifier.config.counterexample.toOption.isDefined) {
+      val model = prover.getModel
+      lastModel = model
+    }
+  }
+
+  protected def assertUsingSoftConstraints(goal: Term): (Boolean, Long) = {
+    endPreamblePhase()
+    val guard = fresh("grd", Nil, sorts.Bool)
+    val guardApp = App(guard, Nil)
+    val goalImplication = Implies(guardApp, goal)
+
+    prover.add(termConverter.convertTerm(goalImplication).asInstanceOf[BoolExpr])
+
+    val startTime = System.currentTimeMillis()
+    val res = prover.check(termConverter.convertTerm(guardApp))
+    val endTime = System.currentTimeMillis()
+    val result = res == Status.UNSATISFIABLE
+    if (!result) {
+      retrieveAndSaveModel()
+    }
+
+    (result, endTime - startTime)
+  }
+
+  def check(timeout: Option[Int] = None): Result = {
+    endPreamblePhase()
+    setTimeout(timeout)
+
+    val res = prover.check()
+
+    res match {
+      case Status.SATISFIABLE => Sat
+      case Status.UNSATISFIABLE => Unsat
+      case Status.UNKNOWN=> Unknown
+    }
+  }
+
+  def endPreamblePhase(): Unit =  {
+    if (!preamblePhaseOver) {
+      preamblePhaseOver = true
+
+      val merged = emittedPreambleString.mkString("\n")
+      val parsed = ctx.parseSMTLIB2String(merged, emittedSortSymbols.toArray, emittedSorts.toArray, emittedFuncSymbols.toArray, emittedFuncs.toArray)
+      prover.add(parsed: _*)
+      prover.add(preambleAssumes.toSeq : _*)
+      preambleAssumes.clear()
+    }
+  }
+
+  def statistics(): Map[String, String] = {
+    val statistics = prover.getStatistics
+    val result = mutable.HashMap[String, String]()
+    for (e <- statistics.getEntries()) {
+      result.update(e.Key, e.getValueString)
+    }
+    ListMap.from(result)
+  }
+
+  def comment(str: String): Unit = {
+    // ignore
+  }
+
+  def fresh(name: String, argSorts: Seq[Sort], resultSort: Sort): Fun = {
+    val id = identifierFactory.fresh(name)
+    val fun = Fun(id, argSorts, resultSort)
+    val decl = FunctionDecl(fun)
+
+    termConverter.convert(decl)
+
+    fun
+  }
+
+  def declare(decl: Decl): Unit = {
+    // We convert the declaration into a Z3-level declaration (which is automatically added to Z3's
+    // current state) and record it in out collection(s) of emmitted declarations.
+    // Special handling for macro declarations if expandMacros is true; in that case,
+    // nothing is declared on the Z3 level, and we simply remember the definition ourselves.
+    decl match {
+      case SortDecl(s) =>
+        val convertedSort = termConverter.convertSort(s)
+        val convertedSortSymbol = termConverter.convertSortSymbol(s)
+        if (convertedSortSymbol.isDefined) {
+          emittedSortSymbols.add(convertedSortSymbol.get)
+          emittedSorts.add(convertedSort)
+        }
+      case fd: FunctionDecl =>
+        val converted = termConverter.convert(fd)
+        if (!emittedFuncs.contains(converted)){
+          emittedFuncs.add(converted)
+          emittedFuncSymbols.append(termConverter.convertFuncSymbol(fd))
+        }
+      case MacroDecl(id, args, body) if expandMacros => termConverter.macros.update(id.name, (args, body))
+      case md: MacroDecl if !expandMacros =>
+        val (convertedFunc, axiom) = termConverter.convert(md)
+        if (!emittedFuncs.contains(convertedFunc)){
+          emittedFuncs.add(convertedFunc)
+          emittedFuncSymbols.append(convertedFunc.getName)
+        }
+        if (preamblePhaseOver){
+          prover.add(axiom)
+        }else{
+          preambleAssumes.add(axiom)
+        }
+      case swd: SortWrapperDecl =>
+        val converted = termConverter.convert(swd)
+        if (!emittedFuncs.contains(converted)){
+          emittedFuncs.add(converted)
+          emittedFuncSymbols.append(termConverter.convertSortWrapperSymbol(swd))
+        }
+    }
+  }
+
+  protected def logToFile(str: String): Unit = {
+    if (logfileWriter != null) {
+      logfileWriter.println(str)
+    }
+  }
+
+  override def getModel(): ViperModel = {
+    val entries = new mutable.HashMap[String, ModelEntry]()
+    for (constDecl <- lastModel.getConstDecls){
+      val constInterp = lastModel.getConstInterp(constDecl)
+      val constName = constDecl.getName.toString
+      val entry = fastparse.parse(constInterp.toString, ModelParser.value(_)).get.value
+      entries.update(constName, entry)
+    }
+    for (funcDecl <- lastModel.getFuncDecls) {
+      val funcInterp = lastModel.getFuncInterp(funcDecl)
+      val options = new mutable.HashMap[Seq[ValueEntry], ValueEntry]()
+      for (entry <- funcInterp.getEntries) {
+        val args = entry.getArgs.map(arg => fastparse.parse(arg.toString, ModelParser.value(_)).get.value)
+        val value = fastparse.parse(entry.getValue.toString, ModelParser.value(_)).get.value
+        options.update(args.toIndexedSeq, value)
+      }
+      val els = fastparse.parse(funcInterp.getElse.toString, ModelParser.value(_)).get.value
+      entries.update(funcDecl.getName.toString, MapEntry(options.toMap, els))
+    }
+    ViperModel(entries.toMap)
+  }
+
+  override def hasModel(): Boolean = {
+    lastModel != null
+  }
+
+  override def isModelValid(): Boolean = {
+    lastModel != null
+  }
+
+  override def clearLastModel(): Unit = lastModel = null
+
+  protected def setTimeout(timeout: Option[Int]): Unit = {
+    val effectiveTimeout = timeout.getOrElse(Verifier.config.proverTimeout)
+
+    /* [2015-07-27 Malte] Setting the timeout unnecessarily often seems to
+     * worsen performance, if only a bit. For the current test suite of
+     * 199 Silver files, the total verification time increased from 60s
+     * to 70s if 'set-option' is emitted every time.
+     */
+    if (lastTimeout != effectiveTimeout) {
+      lastTimeout = effectiveTimeout
+
+      if(Verifier.config.proverEnableResourceBounds) {
+        ctx.updateParamValue("rlimit", (effectiveTimeout * Verifier.config.proverResourcesPerMillisecond).toString)
+      } else {
+        ctx.updateParamValue("timeout", effectiveTimeout.toString)
+      }
+    }
+  }
+
+  lazy val name: String = Z3ProverAPI.name
+
+  lazy val minVersion: Version = Z3ProverAPI.minVersion
+
+  lazy val maxVersion: Option[Version] = Z3ProverAPI.maxVersion
+
+  lazy val staticPreamble: String = Z3ProverAPI.staticPreamble
+
+  lazy val randomizeSeedsOptions: Seq[String] = {
+    Seq(Z3ProverAPI.randomizeSeedsSetting)
+  }
+}
diff --git a/src/main/scala/decider/Z3ProverStdIO.scala b/src/main/scala/decider/Z3ProverStdIO.scala
index 9632b9922..3c4fd69cb 100644
--- a/src/main/scala/decider/Z3ProverStdIO.scala
+++ b/src/main/scala/decider/Z3ProverStdIO.scala
@@ -64,4 +64,6 @@ class Z3ProverStdIO(uniqueId: String,
   protected def getProverPath: Path = {
     Paths.get(Verifier.config.z3Exe)
   }
+
+  override def emitSettings(contents: Iterable[String]): Unit = emit(contents)
 }
diff --git a/src/main/scala/interfaces/Preamble.scala b/src/main/scala/interfaces/Preamble.scala
index 6f9b895bb..66a7ba7b9 100644
--- a/src/main/scala/interfaces/Preamble.scala
+++ b/src/main/scala/interfaces/Preamble.scala
@@ -14,10 +14,10 @@ trait PreambleReader[I, O] {
   def readPreamble(resource: I): Iterable[O]
   def readParametricPreamble(resource: String, substitutions: Map[I, O]): Iterable[O]
 
-  def emitPreamble(preamble: Iterable[O], sink: ProverLike): Unit
+  def emitPreamble(preamble: Iterable[O], sink: ProverLike, isOptions: Boolean): Unit
 
-  def emitPreamble(resource: I, sink: ProverLike): Unit = {
-    emitPreamble(readPreamble(resource), sink)
+  def emitPreamble(resource: I, sink: ProverLike, isOptions: Boolean): Unit = {
+    emitPreamble(readPreamble(resource), sink, isOptions)
   }
 
   def emitParametricPreamble(resource: String, substitutions: Map[I, O], sink: ProverLike): Unit
diff --git a/src/main/scala/interfaces/decider/Prover.scala b/src/main/scala/interfaces/decider/Prover.scala
index 4ff70905f..e61444d94 100644
--- a/src/main/scala/interfaces/decider/Prover.scala
+++ b/src/main/scala/interfaces/decider/Prover.scala
@@ -6,9 +6,11 @@
 
 package viper.silicon.interfaces.decider
 
+import viper.silicon.common.config.Version
 import viper.silver.components.StatefulComponent
 import viper.silicon.{Config, Map}
 import viper.silicon.state.terms._
+import viper.silver.verifier.Model
 
 sealed abstract class Result
 object Sat extends Result
@@ -19,6 +21,7 @@ object Unknown extends Result
 trait ProverLike {
   def emit(content: String): Unit
   def emit(contents: Iterable[String]): Unit = { contents foreach emit }
+  def emitSettings(contents: Iterable[String]): Unit
   def assume(term: Term): Unit
   def declare(decl: Decl): Unit
   def comment(content: String): Unit
@@ -31,6 +34,21 @@ trait Prover extends ProverLike with StatefulComponent {
   def check(timeout: Option[Int] = None): Result
   def fresh(id: String, argSorts: Seq[Sort], resultSort: Sort): Function
   def statistics(): Map[String, String]
-  def getLastModel(): String
+  def hasModel(): Boolean
+  def isModelValid(): Boolean
+  def getModel(): Model
   def clearLastModel(): Unit
+
+  def name: String
+  def minVersion: Version
+  def maxVersion: Option[Version]
+  def version(): Version
+  def staticPreamble: String
+  def randomizeSeedsOptions: Seq[String]
+
+  def pushPopScopeDepth: Int
+
+  def push(n: Int = 1): Unit
+
+  def pop(n: Int = 1): Unit
 }
diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala
index c184a6e0a..427561677 100644
--- a/src/main/scala/rules/Brancher.scala
+++ b/src/main/scala/rules/Brancher.scala
@@ -7,11 +7,14 @@
 package viper.silicon.rules
 
 import java.util.concurrent._
+
+import viper.silicon.common.collections.immutable
 import viper.silicon.common.concurrency._
+import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces.{Unreachable, VerificationResult}
 import viper.silicon.logger.SymbExLogger
 import viper.silicon.state.State
-import viper.silicon.state.terms.{Not, Term}
+import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
 
@@ -38,7 +41,7 @@ object brancher extends BranchingRules {
 
     val negatedCondition = Not(condition)
     val negatedConditionExp = conditionExp.fold[Option[ast.Exp]](None)(c => Some(ast.Not(c)(pos = conditionExp.get.pos, info = conditionExp.get.info, ast.NoTrafos)))
-    val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin
+
 
     /* Skip path feasibility check if one of the following holds:
      *   (1) the branching is due to the short-circuiting evaluation of a conjunction
@@ -61,6 +64,8 @@ object brancher extends BranchingRules {
       || skipPathFeasibilityCheck
       || !v.decider.check(condition, Verifier.config.checkTimeout()))
 
+    val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin && executeThenBranch && executeElseBranch
+
 //    val additionalPaths =
 //      if (executeThenBranch && exploreFalseBranch) 1
 //      else 0
@@ -76,6 +81,9 @@ object brancher extends BranchingRules {
     v.decider.prover.comment(elseBranchComment)
 
     val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(2, Some(condition))
+    var functionsOfCurrentDecider: immutable.InsertionOrderedSet[FunctionDecl] = null
+    var macrosOfCurrentDecider: Vector[MacroDecl] = null
+    var pcsOfCurrentDecider: PathConditionStack = null
 
     val elseBranchVerificationTask: Verifier => VerificationResult =
       if (executeElseBranch) {
@@ -87,40 +95,34 @@ object brancher extends BranchingRules {
          * needed, the second one ensures that the current path conditions (etc.) of the
          * "offloading" verifier are captured.
          */
-//        val functionsOfCurrentDecider = v.decider.freshFunctions
-//        val macrosOfCurrentDecider = v.decider.freshMacros
-//        val pcsOfCurrentDecider = v.decider.pcs.duplicate()
-
-//        println(s"\n[INIT elseBranchVerificationTask v.uniqueId = ${v.uniqueId}]")
-//        println(s"  condition = $condition")
-//        println("  v.decider.pcs.assumptions = ")
-//        v.decider.pcs.assumptions foreach (a => println(s"    $a"))
-//        println("  v.decider.pcs.branchConditions = ")
-//        v.decider.pcs.branchConditions foreach (a => println(s"    $a"))
+        if (parallelizeElseBranch){
+          functionsOfCurrentDecider = v.decider.freshFunctions
+          macrosOfCurrentDecider = v.decider.freshMacros
+          pcsOfCurrentDecider = v.decider.pcs.duplicate()
+        }
 
         (v0: Verifier) => {
           SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
           SymbExLogger.currentLog().markReachable(uidBranchPoint)
-          executionFlowController.locally(s, v0)((s1, v1) => {
-            if (v.uniqueId != v1.uniqueId) {
+          if (v.uniqueId != v0.uniqueId){
+            /* [BRANCH-PARALLELISATION] */
+            // executing the else branch on a different verifier, need to adapt the state
 
-              /* [BRANCH-PARALLELISATION] */
-              throw new RuntimeException("Branch parallelisation is expected to be deactivated for now")
+            // TODO: These seem to be ListSets, for which subtraction is O(n^2). Maybe replace with LinkedHashSets?
+            val newFunctions = functionsOfCurrentDecider -- v0.decider.freshFunctions
+            val newMacros = macrosOfCurrentDecider.diff(v0.decider.freshMacros)
 
-//                val newFunctions = functionsOfCurrentDecider -- v1.decider.freshFunctions
-//                val newMacros = macrosOfCurrentDecider.diff(v1.decider.freshMacros)
-//
-//                v1.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v1.uniqueId}]")
-//                v1.decider.prover.comment(s"Bulk-declaring functions")
-//                v1.decider.declareAndRecordAsFreshFunctions(newFunctions)
-//                v1.decider.prover.comment(s"Bulk-declaring macros")
-//                v1.decider.declareAndRecordAsFreshMacros(newMacros)
-//
-//                v1.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
-//                v1.decider.setPcs(pcsOfCurrentDecider)
-//                v1.decider.pcs.pushScope() /* Empty scope for which the branch condition can be set */
-            }
+            v0.decider.prover.comment(s"[Shifting execution from ${v.uniqueId} to ${v0.uniqueId}]")
+            v0.decider.prover.comment(s"Bulk-declaring functions")
+            v0.decider.declareAndRecordAsFreshFunctions(newFunctions)
+            v0.decider.prover.comment(s"Bulk-declaring macros")
+            v0.decider.declareAndRecordAsFreshMacros(newMacros)
+
+            v0.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
+            v0.decider.setPcs(pcsOfCurrentDecider)
 
+          }
+          executionFlowController.locally(s, v0)((s1, v1) => {
             v1.decider.prover.comment(s"[else-branch: $cnt | $negatedCondition]")
             v1.decider.setCurrentBranchCondition(negatedCondition, negatedConditionExp)
 
@@ -135,15 +137,11 @@ object brancher extends BranchingRules {
       if (executeElseBranch) {
         if (parallelizeElseBranch) {
           /* [BRANCH-PARALLELISATION] */
-          throw new RuntimeException("Branch parallelisation is expected to be deactivated for now")
-//          v.verificationPoolManager.queueVerificationTask(v0 => {
-//            v0.verificationPoolManager.runningVerificationTasks.put(elseBranchVerificationTask, true)
-//            val res = elseBranchVerificationTask(v0)
-//
-//            v0.verificationPoolManager.runningVerificationTasks.remove(elseBranchVerificationTask)
-//
-//            Seq(res)
-//          })
+          v.verificationPoolManager.queueVerificationTask(v0 => {
+            val res = elseBranchVerificationTask(v0)
+
+            Seq(res)
+          })
         } else {
           new SynchronousFuture(Seq(elseBranchVerificationTask(v)))
         }
@@ -164,37 +162,31 @@ object brancher extends BranchingRules {
     }) combine {
 
       /* [BRANCH-PARALLELISATION] */
-      if (parallelizeElseBranch) {
-//          && v.verificationPoolManager.slaveVerifierPool.getNumIdle == 0
-//          && !v.verificationPoolManager.runningVerificationTasks.containsKey(elseBranchVerificationTask)
-//                /* TODO: This attempt to ensure that the elseBranchVerificationTask is not already
-//                 *       being executed is most likely not thread-safe since checking if a task
-//                 *       is still in the queue and canceling it, if so, is not an atomic operation.
-//                 *       I.e. the task may be taken out of the queue in between.
-//                 */
-
-        throw new RuntimeException("Branch parallelisation is expected to be deactivated for now")
-
-//        /* Cancelling the task should result in the underlying task being removed from the task
-//         * queue/executor
-//         */
-//        elseBranchFuture.cancel(true)
-//
-//        /* Run the task on the current thread */
-//        elseBranchVerificationTask(v)
-      } else {
-        var rs: Seq[VerificationResult] = null
-        try {
+      var rs: Seq[VerificationResult] = null
+      try {
+        if (parallelizeElseBranch) {
+          pcsOfCurrentDecider = v.decider.pcs.duplicate()
+
+          val pcsBefore = v.decider.pcs
+
           rs = elseBranchFuture.get()
-        } catch {
-          case ex: ExecutionException =>
-            ex.getCause.printStackTrace()
-            throw ex
-        }
 
-        assert(rs.length == 1, s"Expected a single verification result but found ${rs.length}")
-        rs.head
+          if (v.decider.pcs != pcsBefore){
+            // we have done other work during the join, need to reset
+            v.decider.setPcs(pcsOfCurrentDecider)
+          }
+        }else{
+          rs = elseBranchFuture.get()
+        }
+      } catch {
+        case ex: ExecutionException =>
+          ex.getCause.printStackTrace()
+          throw ex
       }
+
+      assert(rs.length == 1, s"Expected a single verification result but found ${rs.length}")
+      rs.head
+
     }
     SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
     res
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 08e30aa66..a3917021b 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -24,6 +24,7 @@ import viper.silicon.state.terms._
 import viper.silicon.state.terms.predef.`?r`
 import viper.silicon.utils.freshSnap
 import viper.silicon.verifier.Verifier
+import viper.silver.cfg.{ConditionalEdge, Kind}
 
 trait ExecutionRules extends SymbolicExecutionRules {
   def exec(s: State,
@@ -101,17 +102,38 @@ object executor extends ExecutionRules {
     } else if (edges.length == 1) {
       follow(s, edges.head, v)(Q)
     } else {
-      val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(edges.length)
-      val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) {
-        case (result: VerificationResult, (edge, edgeIndex)) =>
-          if (edgeIndex != 0) {
-            SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
+      edges match {
+        case Seq(thenEdge@ConditionalEdge(cond1, _, _, Kind.Normal), elseEdge@ConditionalEdge(cond2, _, _, Kind.Normal))
+            if Verifier.config.parallelizeBranches() && cond2 == ast.Not(cond1)()  =>
+          val condEdgeRecord = new ConditionalEdgeRecord(thenEdge.condition, s, v.decider.pcs)
+          val sepIdentifier = SymbExLogger.currentLog().openScope(condEdgeRecord)
+          val res = eval(s, thenEdge.condition, IfFailed(thenEdge.condition), v)((s2, tCond, v1) =>
+            brancher.branch(s2, tCond, Some(thenEdge.condition), v1)(
+              (s3, v3) =>
+                exec(s3, thenEdge.target, thenEdge.kind, v3)((s4, v4) => {
+                  SymbExLogger.currentLog().closeScope(sepIdentifier)
+                  val branchRes = Q(s4, v4)
+                  branchRes
+                }),
+              (s3, v3) =>
+                exec(s3, elseEdge.target, elseEdge.kind, v3)((s4, v4) => {
+                  SymbExLogger.currentLog().closeScope(sepIdentifier)
+                  Q(s4, v4)
+                })))
+          res
+        case _ =>
+          val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(edges.length)
+          val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) {
+            case (result: VerificationResult, (edge, edgeIndex)) =>
+              if (edgeIndex != 0) {
+                SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
+              }
+              SymbExLogger.currentLog().markReachable(uidBranchPoint)
+              result combine follow(s, edge, v)(Q)
           }
-          SymbExLogger.currentLog().markReachable(uidBranchPoint)
-          result combine follow(s, edge, v)(Q)
+          SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
+          res
       }
-      SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
-      res
     }
   }
 
@@ -176,7 +198,7 @@ object executor extends ExecutionRules {
                 produces(s0, freshSnap, invs, ContractNotWellformed, v0)((s1, v1) => {
                   phase1data = phase1data :+ (s1,
                                               v1.decider.pcs.after(mark),
-                                              InsertionOrderedSet.empty[FunctionDecl] /*v2.decider.freshFunctions*/ /* [BRANCH-PARALLELISATION] */)
+                                              v1.decider.freshFunctions /* [BRANCH-PARALLELISATION] */)
                   v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions")
                   edgeConditions.foldLeft(Success(): VerificationResult) {
                     case (fatalResult: FatalResult, _) => fatalResult
@@ -190,10 +212,10 @@ object executor extends ExecutionRules {
                   v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)")
                   phase1data.foldLeft(Success(): VerificationResult) {
                     case (fatalResult: FatalResult, _) => fatalResult
-                    case (intermediateResult, (s1, pcs, _)) => /* [BRANCH-PARALLELISATION] ff1 */
+                    case (intermediateResult, (s1, pcs, ff1)) => /* [BRANCH-PARALLELISATION] ff1 */
                       val s2 = s1.copy(invariantContexts = sLeftover.h +: s1.invariantContexts)
                       intermediateResult && executionFlowController.locally(s2, v1)((s3, v2) => {
-  //                    v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */
+                        v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */
                         v2.decider.assume(pcs.assumptions)
                         v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
                         if (v2.decider.checkSmoke())
diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala
index 0fdbe20ca..31f1b98d0 100644
--- a/src/main/scala/rules/SymbolicExecutionRules.scala
+++ b/src/main/scala/rules/SymbolicExecutionRules.scala
@@ -11,7 +11,7 @@ import viper.silicon.state.State
 import viper.silicon.verifier.Verifier
 import viper.silver.frontend.{MappedModel, NativeModel, VariablesModel}
 import viper.silver.verifier.errors.ErrorWrapperWithExampleTransformer
-import viper.silver.verifier.{Counterexample, CounterexampleTransformer, Model, VerificationError}
+import viper.silver.verifier.{Counterexample, CounterexampleTransformer, VerificationError}
 
 trait SymbolicExecutionRules {
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, generateNewModel: Boolean = false): Failure = {
@@ -24,12 +24,11 @@ trait SymbolicExecutionRules {
       case _ => ve
     }
     val counterexample: Option[Counterexample] = if (v != null && Verifier.config.counterexample.toOption.isDefined) {
-      if (generateNewModel || v.decider.getModel() == null) {
+      if (generateNewModel || !v.decider.hasModel()) {
         v.decider.generateModel()
       }
-      val model = v.decider.getModel()
-      if (model != null && !model.contains("model is not available")) {
-        val nativeModel = Model(model)
+      if (v.decider.isModelValid()) {
+        val nativeModel = v.decider.getModel()
         val ce_type = Verifier.config.counterexample()
         val ce: Counterexample = ce_type match {
           case NativeModel =>
diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala
index 421d05e5a..c0d085525 100644
--- a/src/main/scala/state/Terms.scala
+++ b/src/main/scala/state/Terms.scala
@@ -2085,15 +2085,15 @@ object SortWrapper {
 
 /* Other terms */
 
-class Distinct(val ts: Set[Symbol]) extends BooleanTerm with StructuralEquality {
+class Distinct(val ts: Set[DomainFun]) extends BooleanTerm with StructuralEquality {
   assert(ts.size >= 2, "Distinct requires at least two terms")
 
   val equalityDefiningMembers = ts :: Nil
   override lazy val toString = s"Distinct($ts)"
 }
 
-object Distinct extends (Set[Symbol] => Term) {
-  def apply(ts: Set[Symbol]): Term =
+object Distinct extends (Set[DomainFun] => Term) {
+  def apply(ts: Set[DomainFun]): Term =
     if (ts.size >= 2) new Distinct(ts)
     else True()
 
diff --git a/src/main/scala/supporters/Domains.scala b/src/main/scala/supporters/Domains.scala
index 7a253b96a..aff3c080a 100644
--- a/src/main/scala/supporters/Domains.scala
+++ b/src/main/scala/supporters/Domains.scala
@@ -28,7 +28,7 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter,
   private var collectedSorts = InsertionOrderedSet[Sort]()
   private var collectedFunctions = InsertionOrderedSet[terms.DomainFun]()
   private var collectedAxioms = InsertionOrderedSet[Term]()
-  private var uniqueSymbols = MultiMap.empty[Sort, Symbol]
+  private var uniqueSymbols = MultiMap.empty[Sort, DomainFun]
 
   /* Lifetime */
 
diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMasterVerifier.scala
index 1120183af..56de055cd 100644
--- a/src/main/scala/verifier/DefaultMasterVerifier.scala
+++ b/src/main/scala/verifier/DefaultMasterVerifier.scala
@@ -108,6 +108,11 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter)
       _verificationPoolManager.pooledVerifiers.emit(content)
     }
 
+    override def emit(contents: Iterable[String]): Unit = {
+      decider.prover.emit(contents)
+      _verificationPoolManager.pooledVerifiers.emit(contents)
+    }
+
     def assume(term: Term): Unit = {
       decider.prover.assume(term)
       _verificationPoolManager.pooledVerifiers.assume(term)
@@ -132,6 +137,11 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter)
       decider.prover.saturate(data)
       _verificationPoolManager.pooledVerifiers.saturate(data)
     }
+
+    override def emitSettings(contents: Iterable[String]): Unit = {
+      decider.prover.emitSettings(contents)
+      _verificationPoolManager.pooledVerifiers.emitSettings(contents)
+    }
   }
 
   /* Program verification */
@@ -230,7 +240,9 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter)
 
     val verificationTaskFutures: Seq[Future[Seq[VerificationResult]]] =
       program.methods.filterNot(excludeMethod).map(method => {
-        val s = createInitialState(method, program, functionData, predicateData)/*.copy(parallelizeBranches = true)*/ /* [BRANCH-PARALLELISATION] */
+
+        val s = createInitialState(method, program, functionData, predicateData).copy(parallelizeBranches =
+          Verifier.config.parallelizeBranches()) /* [BRANCH-PARALLELISATION] */
 
         _verificationPoolManager.queueVerificationTask(v => {
           val startTime = System.currentTimeMillis()
@@ -243,7 +255,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter)
           setErrorScope(results, method)
         })
       }) ++ cfgs.map(cfg => {
-        val s = createInitialState(cfg, program, functionData, predicateData)/*.copy(parallelizeBranches = true)*/ /* [BRANCH-PARALLELISATION] */
+        val s = createInitialState(cfg, program, functionData, predicateData).copy(parallelizeBranches = true) /* [BRANCH-PARALLELISATION] */
 
         _verificationPoolManager.queueVerificationTask(v => {
           val startTime = System.currentTimeMillis()
@@ -317,14 +329,14 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter)
 
   private def emitStaticPreamble(sink: ProverLike): Unit = {
     sink.comment(s"\n; ${decider.prover.staticPreamble}")
-    preambleReader.emitPreamble(decider.prover.staticPreamble, sink)
+    preambleReader.emitPreamble(decider.prover.staticPreamble, sink, true)
 
     if (config.proverRandomizeSeeds) {
       sink.comment(s"\n; Randomise seeds [--${config.rawProverRandomizeSeeds.name}]")
       val options = decider.prover.randomizeSeedsOptions
         .map (key => s"(set-option :$key ${Random.nextInt(10000)})")
 
-      preambleReader.emitPreamble(options, sink)
+      preambleReader.emitPreamble(options, sink, true)
     }
 
     val smt2ConfigOptions =
@@ -335,11 +347,11 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter)
       val msg = s"Additional prover configuration options are '${config.proverConfigArgs}'"
       reporter report ConfigurationConfirmation(msg)
       logger info msg
-      preambleReader.emitPreamble(smt2ConfigOptions, sink)
+      preambleReader.emitPreamble(smt2ConfigOptions, sink, true)
     }
 
     sink.comment("\n; /preamble.smt2")
-    preambleReader.emitPreamble("/preamble.smt2", sink)
+    preambleReader.emitPreamble("/preamble.smt2", sink, false)
   }
 
   /* Prover preamble: After program analysis */
diff --git a/src/main/scala/verifier/VerificationPoolManager.scala b/src/main/scala/verifier/VerificationPoolManager.scala
index 02139cedb..57ee41bc2 100644
--- a/src/main/scala/verifier/VerificationPoolManager.scala
+++ b/src/main/scala/verifier/VerificationPoolManager.scala
@@ -19,13 +19,12 @@ class VerificationPoolManager(master: MasterVerifier) extends StatefulComponent
   private val numberOfSlaveVerifiers: Int = Verifier.config.numberOfParallelVerifiers()
 
   /*private*/ var slaveVerifiers: Seq[SlaveVerifier] = _
-  /*private*/ var slaveVerifierExecutor: ExecutorService = _
+  /*private*/ var slaveVerifierExecutor: ForkJoinPool = _
   /*private*/ var slaveVerifierPool: ObjectPool[SlaveVerifier] = _
 
-  /* private */ var runningVerificationTasks: ConcurrentHashMap[AnyRef, Boolean] = _
-
   private[verifier] object pooledVerifiers extends ProverLike {
     def emit(content: String): Unit = slaveVerifiers foreach (_.decider.prover.emit(content))
+    override def emit(contents: Iterable[String]): Unit = slaveVerifiers foreach (_.decider.prover.emit(contents))
     def assume(term: Term): Unit = slaveVerifiers foreach (_.decider.prover.assume(term))
     def declare(decl: Decl): Unit =  slaveVerifiers foreach (_.decider.prover.declare(decl))
     def comment(content: String): Unit = slaveVerifiers foreach (_.decider.prover.comment(content))
@@ -35,13 +34,15 @@ class VerificationPoolManager(master: MasterVerifier) extends StatefulComponent
 
     def saturate(timeout: Int, comment: String): Unit =
       slaveVerifiers foreach (_.decider.prover.saturate(timeout, comment))
+
+    override def emitSettings(contents: Iterable[String]): Unit =
+      slaveVerifiers foreach (_.decider.prover.emitSettings(contents))
   }
 
   /* Verifier pool management */
 
   private def setupSlaveVerifierPool(): Unit = {
     slaveVerifiers = Vector.empty
-    runningVerificationTasks = new ConcurrentHashMap()
 
     val poolConfig: GenericObjectPoolConfig[SlaveVerifier] = new GenericObjectPoolConfig()
     poolConfig.setMaxTotal(numberOfSlaveVerifiers)
@@ -50,29 +51,24 @@ class VerificationPoolManager(master: MasterVerifier) extends StatefulComponent
 
     val factory = PoolUtils.synchronizedPooledFactory(slaveVerifierPoolableObjectFactory)
 
-    slaveVerifierPool =
-    //    PoolUtils.synchronizedPool(
-    new GenericObjectPool[SlaveVerifier](factory, poolConfig)
-    //    )
+    slaveVerifierPool = new GenericObjectPool[SlaveVerifier](factory, poolConfig)
 
     slaveVerifierPool.addObjects(poolConfig.getMaxTotal)
-    //  Thread.sleep(2000)
 
     assert(slaveVerifiers.length == poolConfig.getMaxTotal)
     slaveVerifiers foreach (_.start())
 
-    slaveVerifierExecutor = Executors.newFixedThreadPool(poolConfig.getMaxTotal)
-//    slaveVerifierExecutor = Executors.newWorkStealingPool(poolConfig.getMaxTotal)
+    slaveVerifierExecutor = new ForkJoinPool(poolConfig.getMaxTotal, new SlaveBorrowingForkJoinThreadFactory(), null, false)
   }
 
   private def resetSlaveVerifierPool(): Unit = {
+    slaveVerifierExecutor.awaitQuiescence(10, TimeUnit.SECONDS)
     slaveVerifiers foreach (_.reset())
-
-    runningVerificationTasks.clear()
   }
 
   private def teardownSlaveVerifierPool(): Unit = {
     if (slaveVerifiers != null) {
+      slaveVerifierExecutor.awaitQuiescence(10, TimeUnit.SECONDS)
       slaveVerifiers foreach (_.stop())
 
       slaveVerifierExecutor.shutdown()
@@ -97,28 +93,15 @@ class VerificationPoolManager(master: MasterVerifier) extends StatefulComponent
 
   /* Verification task management */
 
-  private final class SlaveBorrowingVerificationTask(task: SlaveVerifier => Seq[VerificationResult])
-      extends Callable[Seq[VerificationResult]] {
-
-    def call(): Seq[VerificationResult] = {
-      var slave: SlaveVerifier = null
-
-      try {
-        slave = slaveVerifierPool.borrowObject()
-
-        task(slave)
-      } finally {
-        if (slave != null) {
-          slaveVerifierPool.returnObject(slave)
-        }
-      }
-    }
-  }
 
   def queueVerificationTask(task: SlaveVerifier => Seq[VerificationResult])
                            : Future[Seq[VerificationResult]] = {
-
-    slaveVerifierExecutor.submit(new SlaveBorrowingVerificationTask(task))
+    val thread = Thread.currentThread()
+    if (thread.isInstanceOf[SlaveBorrowingForkJoinWorkerThread]){
+      new SlaveAwareForkJoinTask(task).fork
+    }else{
+      slaveVerifierExecutor.submit(new SlaveAwareForkJoinTask(task))
+    }
   }
 
   /* Lifetime */
@@ -134,4 +117,39 @@ class VerificationPoolManager(master: MasterVerifier) extends StatefulComponent
   def stop(): Unit = {
     teardownSlaveVerifierPool()
   }
+
+  class SlaveBorrowingForkJoinThreadFactory extends ForkJoinPool.ForkJoinWorkerThreadFactory {
+    override def newThread(forkJoinPool: ForkJoinPool): ForkJoinWorkerThread = {
+      new SlaveBorrowingForkJoinWorkerThread(forkJoinPool)
+    }
+  }
+
+  class SlaveBorrowingForkJoinWorkerThread(pool: ForkJoinPool) extends ForkJoinWorkerThread(pool) {
+    // each thread has its own slave verifier that does not change.
+    var slave: SlaveVerifier = null
+
+    override def onStart(): Unit = {
+      slave = slaveVerifierPool.borrowObject()
+    }
+
+    override def onTermination(exception: Throwable): Unit = {
+      if (slave != null) {
+        slaveVerifierPool.returnObject(slave)
+      }
+    }
+
+  }
+
+  class SlaveAwareForkJoinTask(task: SlaveVerifier => Seq[VerificationResult])
+    extends RecursiveTask[Seq[VerificationResult]]{
+
+    override def compute(): Seq[VerificationResult] = {
+      // get the slave verifier of the current thread
+      val worker = Thread.currentThread().asInstanceOf[SlaveBorrowingForkJoinWorkerThread]
+      val slave = worker.slave
+      task(slave)
+    }
+  }
 }
+
+
diff --git a/src/test/scala/SiliconTestsParallelBranches.scala b/src/test/scala/SiliconTestsParallelBranches.scala
new file mode 100644
index 000000000..03a3ffbd7
--- /dev/null
+++ b/src/test/scala/SiliconTestsParallelBranches.scala
@@ -0,0 +1,15 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2022 ETH Zurich.
+
+package viper.silicon.tests
+
+class SiliconTestsParallelBranches extends SiliconTests {
+  override val testDirectories: Seq[String] = Seq("examples")
+
+ override val commandLineArguments: Seq[String] = Seq(
+    "--timeout", "300" /* seconds */,
+    "--parallelizeBranches")
+}