From c667d67d43f64e3efcddc8bcd6a50c2c1ee8f7fe Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 7 Jun 2023 17:34:02 +0200
Subject: [PATCH 01/61] Auto-including decreases functions and axioms when they
 are used

---
 .../silver/frontend/ViperPAstProvider.scala   | 100 ++++++++++++++++++
 .../termination/TerminationPlugin.scala       |  80 +++++++++++++-
 .../errorMessages/multipleErrors.vpr          |   1 -
 .../termination/functions/basic/adt.vpr       |   1 -
 .../termination/functions/basic/allTypes.vpr  |   2 +-
 .../existingExamples/McCarthys91Fnc.sil       |   1 -
 6 files changed, 179 insertions(+), 6 deletions(-)
 create mode 100644 src/main/scala/viper/silver/frontend/ViperPAstProvider.scala

diff --git a/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala
new file mode 100644
index 000000000..8d8757cce
--- /dev/null
+++ b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala
@@ -0,0 +1,100 @@
+// 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.silver.frontend
+
+
+import ch.qos.logback.classic.Logger
+import viper.silver.ast.Program
+import viper.silver.logger.ViperStdOutLogger
+import viper.silver.plugin.SilverPluginManager
+import viper.silver.reporter.{AstConstructionFailureMessage, AstConstructionSuccessMessage, Reporter}
+import viper.silver.verifier.{Failure, Success, VerificationResult, Verifier}
+
+import java.nio.file.Path
+
+
+class ViperPAstProvider(override val reporter: Reporter,
+                        override implicit val logger: Logger = ViperStdOutLogger("ViperPAstProvider", "INFO").get,
+                        private val disablePlugins: Boolean = false) extends SilFrontend {
+
+  class Config(args: Seq[String]) extends SilFrontendConfig(args, "ViperPAstProviderConfig") {
+    verify()
+  }
+
+  class PAstProvidingVerifier(rep: Reporter) extends Verifier {
+    private var _config: Config = _
+
+    def config: Config = _config
+
+    override def name = "Viper PAST Constructor"
+
+    override def version = ""
+
+    override def buildVersion = ""
+
+    override def copyright: String = "(c) Copyright ETH Zurich 2012 - 2023"
+
+    override def signature: String = name
+
+    override def debugInfo(info: Seq[(String, Any)]): Unit = {}
+
+    override def dependencies: Seq[Nothing] = Nil
+
+    override def start(): Unit = ()
+
+    override def stop(): Unit = {}
+
+    override def verify(program: Program): VerificationResult = Success
+
+    override def parseCommandLine(args: Seq[String]): Unit = {
+      _config = new Config(args)
+    }
+
+    override def reporter: Reporter = rep
+  }
+
+  // All phases after sematic analysis omitted
+  override val phases: Seq[Phase] = Seq(Parsing, SemanticAnalysis)
+
+  override def result: VerificationResult = {
+
+    if (_errors.isEmpty) {
+      require(state >= DefaultStates.SemanticAnalysis)
+      Success
+    }
+    else {
+      Failure(_errors)
+    }
+  }
+
+  protected var instance: PAstProvidingVerifier = _
+
+  override def createVerifier(fullCmd: String): Verifier = {
+    instance = new PAstProvidingVerifier(reporter)
+    instance
+  }
+
+  override def configureVerifier(args: Seq[String]): SilFrontendConfig = {
+    instance.parseCommandLine(args)
+    instance.config
+  }
+
+  override def reset(input: Path): Unit = {
+    super.reset(input)
+    if (_config != null) {
+      noPluginsManager = SilverPluginManager(None)(reporter, logger, _config, fp)
+    }
+  }
+
+  private var noPluginsManager = SilverPluginManager(None)(reporter, logger, _config, fp)
+  override def plugins: SilverPluginManager = {
+    if (disablePlugins) noPluginsManager
+    else {
+      super.plugins
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 8baa5fb3d..86960b7ed 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -16,8 +16,10 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
 import viper.silver.verifier.errors.AssertFailed
 import viper.silver.verifier._
 import fastparse._
+import viper.silver.frontend.{DefaultStates, ViperPAstProvider}
+import viper.silver.logger.SilentLogger
 import viper.silver.parser.FastParserCompanion.whitespace
-import viper.silver.reporter.Entity
+import viper.silver.reporter.{Entity, NoopReporter}
 
 import scala.annotation.unused
 
@@ -29,6 +31,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
 
   private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)
 
+  private var decreasesClauses: Set[PDecreasesClause] = Set.empty
+
   /**
    * Keyword used to define decreases clauses
    */
@@ -95,7 +99,12 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
 
     // Apply the predicate access to instance transformation only to decreases clauses.
     val newProgram: PProgram = StrategyBuilder.Slim[PNode]({
-      case dt: PDecreasesTuple => transformPredicateInstances.execute(dt): PDecreasesTuple
+      case dt: PDecreasesTuple =>
+        decreasesClauses = decreasesClauses + dt
+        transformPredicateInstances.execute(dt): PDecreasesTuple
+      case dc : PDecreasesClause =>
+        decreasesClauses = decreasesClauses + dc
+        dc
       case d => d
     }).recurseFunc({ // decreases clauses can only appear in functions/methods pres and methods bodies
       case PProgram(_, _, _, _, functions, _, methods, _, _) => Seq(functions, methods)
@@ -106,6 +115,73 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     newProgram
   }
 
+  override def beforeTranslate(input: PProgram): PProgram = {
+    val allClauses = decreasesClauses.flatMap{
+      case PDecreasesTuple(exps, _) => exps.map(e => e.typ match {
+        case PUnknown() if e.isInstanceOf[PCall] => e.asInstanceOf[PCall].idnuse.typ
+        case _ => e.typ
+      })
+      case _ => Seq()
+    }
+    val presentDomains = input.domains.map(_.idndef.name).toSet
+
+    val importStmts = allClauses flatMap {
+      case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import <decreases/int.vpr>")
+      case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import <decreases/ref.vpr>")
+      case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import <decreases/bool.vpr>")
+      case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") => Some("import <decreases/rational.vpr>")
+      case PMultisetType(_) if !presentDomains.contains("MultiSetWellFoundedOrder") => Some("import <decreases/multiset.vpr>")
+      case PSeqType(_) if !presentDomains.contains("SeqWellFoundedOrder") => Some("import <decreases/seq.vpr>")
+      case PSetType(_) if !presentDomains.contains("SetWellFoundedOrder") => Some("import <decreases/set.vpr>")
+      case PPredicateType() if !presentDomains.contains("PredicateInstancesWellFoundedOrder") =>
+        Some("import <decreases/predicate_instance.vpr>")
+      case _ => None
+    }
+    if (importStmts.nonEmpty) {
+      val importOnlyProgram = importStmts.mkString("\n")
+      val importPProgram = PAstProvider.generateViperPAst(importOnlyProgram)
+      val mergedDomains = input.domains.filter(_.idndef.name != "WellFoundedOrder") ++ importPProgram.get.domains
+
+      val mergedProgram = input.copy(domains = mergedDomains)(input.pos)
+      super.beforeTranslate(mergedProgram)
+    } else {
+      super.beforeTranslate(input)
+    }
+  }
+
+  object PAstProvider extends ViperPAstProvider(NoopReporter, SilentLogger().get) {
+    def generateViperPAst(code: String): Option[PProgram] = {
+      val code_id = code.hashCode.asInstanceOf[Short].toString
+      _input = Some(code)
+      execute(Array("--ignoreFile", code_id))
+
+      if (errors.isEmpty) {
+        Some(semanticAnalysisResult)
+      } else {
+        None
+      }
+    }
+
+    def setCode(code: String): Unit = {
+      _input = Some(code)
+    }
+
+    override def reset(input: java.nio.file.Path): Unit = {
+      if (state < DefaultStates.Initialized) sys.error("The translator has not been initialized.")
+      _state = DefaultStates.InputSet
+      _inputFile = Some(input)
+
+      /** must be set by [[setCode]] */
+      // _input = None
+      _errors = Seq()
+      _parsingResult = None
+      _semanticAnalysisResult = None
+      _verificationResult = None
+      _program = None
+      resetMessages()
+    }
+  }
+
 
   /**
    * Remove decreases clauses from the AST and add them as information to the AST nodes
diff --git a/src/test/resources/termination/errorMessages/multipleErrors.vpr b/src/test/resources/termination/errorMessages/multipleErrors.vpr
index 1873155f9..3b2425f7a 100644
--- a/src/test/resources/termination/errorMessages/multipleErrors.vpr
+++ b/src/test/resources/termination/errorMessages/multipleErrors.vpr
@@ -4,7 +4,6 @@
 // failure filtering by Silicon should not filter out one of the failures but correctly return both errors
 
 import <decreases/int.vpr>
-import <decreases/predicate_instance.vpr>
 
 function factorialPure(n: Int): Int
     decreases // wrong termination measure
diff --git a/src/test/resources/termination/functions/basic/adt.vpr b/src/test/resources/termination/functions/basic/adt.vpr
index ffb07d25e..54095d7a2 100644
--- a/src/test/resources/termination/functions/basic/adt.vpr
+++ b/src/test/resources/termination/functions/basic/adt.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-import <decreases/int.vpr>
 
 domain list {
 
diff --git a/src/test/resources/termination/functions/basic/allTypes.vpr b/src/test/resources/termination/functions/basic/allTypes.vpr
index 12df6c866..04aa18733 100644
--- a/src/test/resources/termination/functions/basic/allTypes.vpr
+++ b/src/test/resources/termination/functions/basic/allTypes.vpr
@@ -1,7 +1,7 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-import <decreases/all.vpr>
+import <decreases/multiset.vpr>
 
 //Example decreasing Int
 function fact(x:Int): Int
diff --git a/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil b/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil
index abc8a33d4..e4e97bee7 100644
--- a/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil
+++ b/src/test/resources/termination/functions/existingExamples/McCarthys91Fnc.sil
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-import <decreases/int.vpr>
 
 function mc(n:Int): Int
 decreases 100-n

From fb41857252d2ef73152ad6775822c495482bfce9 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 7 Jun 2023 23:55:21 +0200
Subject: [PATCH 02/61] Properly handling unknown types, empty decreases
 clauses

---
 .../standard/termination/TerminationPlugin.scala    |  4 +++-
 .../functions/basic/unconstrainedType.vpr           | 13 +++++++++++++
 .../termination/functions/expressions/forall.vpr    |  1 -
 3 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/termination/functions/basic/unconstrainedType.vpr

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 86960b7ed..bbf4f10f9 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -116,7 +116,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   }
 
   override def beforeTranslate(input: PProgram): PProgram = {
-    val allClauses = decreasesClauses.flatMap{
+    val allClauses: Set[Any] = decreasesClauses.flatMap{
+      case PDecreasesTuple(Seq(), _) => Seq(())
       case PDecreasesTuple(exps, _) => exps.map(e => e.typ match {
         case PUnknown() if e.isInstanceOf[PCall] => e.asInstanceOf[PCall].idnuse.typ
         case _ => e.typ
@@ -135,6 +136,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       case PSetType(_) if !presentDomains.contains("SetWellFoundedOrder") => Some("import <decreases/set.vpr>")
       case PPredicateType() if !presentDomains.contains("PredicateInstancesWellFoundedOrder") =>
         Some("import <decreases/predicate_instance.vpr>")
+      case _ if !presentDomains.contains("WellFoundedOrder") => Some("import <decreases/declaration.vpr>")
       case _ => None
     }
     if (importStmts.nonEmpty) {
diff --git a/src/test/resources/termination/functions/basic/unconstrainedType.vpr b/src/test/resources/termination/functions/basic/unconstrainedType.vpr
new file mode 100644
index 000000000..07ebd45ae
--- /dev/null
+++ b/src/test/resources/termination/functions/basic/unconstrainedType.vpr
@@ -0,0 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain Huh {}
+
+function fac(i: Int, h: Huh): Int
+  requires i >= 0
+  decreases h
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  i == 0 ? 1 : i * fac(i - 1, h)
+}
\ No newline at end of file
diff --git a/src/test/resources/termination/functions/expressions/forall.vpr b/src/test/resources/termination/functions/expressions/forall.vpr
index e1ebb0c82..dbcb61004 100644
--- a/src/test/resources/termination/functions/expressions/forall.vpr
+++ b/src/test/resources/termination/functions/expressions/forall.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-import <decreases/declaration.vpr>
 
 field f: Int
 

From 273c8c53da4fe37d901437ff452db8c67f381c17 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 8 Jun 2023 00:26:15 +0200
Subject: [PATCH 03/61] Removed now invalid test, fixed issue of equal
 decreases expressions disappearing (because sets), fixed typo in multiset
 well-def domain

---
 .../resources/import/decreases/multiset.vpr   |  2 +-
 .../termination/TerminationPlugin.scala       | 12 ++++-----
 .../termination/errorMessages/notDefined.vpr  | 27 -------------------
 3 files changed, 7 insertions(+), 34 deletions(-)
 delete mode 100644 src/test/resources/termination/errorMessages/notDefined.vpr

diff --git a/src/main/resources/import/decreases/multiset.vpr b/src/main/resources/import/decreases/multiset.vpr
index 6ad7e8d8d..b129b69b0 100644
--- a/src/main/resources/import/decreases/multiset.vpr
+++ b/src/main/resources/import/decreases/multiset.vpr
@@ -3,7 +3,7 @@
 
 import "declaration.vpr"
 
-domain MuliSetWellFoundedOrder[S]{
+domain MultiSetWellFoundedOrder[S]{
     //MultiSet
     axiom multiset_ax_dec{
         forall mSet1: Multiset[S], mSet2: Multiset[S] :: {decreasing(mSet1, mSet2)}
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index bbf4f10f9..6f83848c6 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -31,7 +31,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
 
   private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)
 
-  private var decreasesClauses: Set[PDecreasesClause] = Set.empty
+  private var decreasesClauses: Seq[PDecreasesClause] = Seq.empty
 
   /**
    * Keyword used to define decreases clauses
@@ -100,10 +100,10 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     // Apply the predicate access to instance transformation only to decreases clauses.
     val newProgram: PProgram = StrategyBuilder.Slim[PNode]({
       case dt: PDecreasesTuple =>
-        decreasesClauses = decreasesClauses + dt
+        decreasesClauses = decreasesClauses :+ dt
         transformPredicateInstances.execute(dt): PDecreasesTuple
       case dc : PDecreasesClause =>
-        decreasesClauses = decreasesClauses + dc
+        decreasesClauses = decreasesClauses :+ dc
         dc
       case d => d
     }).recurseFunc({ // decreases clauses can only appear in functions/methods pres and methods bodies
@@ -116,17 +116,17 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   }
 
   override def beforeTranslate(input: PProgram): PProgram = {
-    val allClauses: Set[Any] = decreasesClauses.flatMap{
+    val allClauseTypes: Set[Any] = decreasesClauses.flatMap{
       case PDecreasesTuple(Seq(), _) => Seq(())
       case PDecreasesTuple(exps, _) => exps.map(e => e.typ match {
         case PUnknown() if e.isInstanceOf[PCall] => e.asInstanceOf[PCall].idnuse.typ
         case _ => e.typ
       })
       case _ => Seq()
-    }
+    }.toSet
     val presentDomains = input.domains.map(_.idndef.name).toSet
 
-    val importStmts = allClauses flatMap {
+    val importStmts = allClauseTypes flatMap {
       case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import <decreases/int.vpr>")
       case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import <decreases/ref.vpr>")
       case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import <decreases/bool.vpr>")
diff --git a/src/test/resources/termination/errorMessages/notDefined.vpr b/src/test/resources/termination/errorMessages/notDefined.vpr
deleted file mode 100644
index 4401cf0b8..000000000
--- a/src/test/resources/termination/errorMessages/notDefined.vpr
+++ /dev/null
@@ -1,27 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-// decreases and bounded functions are not imported
-
-function f(x: Int): Int
-    //:: ExpectedOutput(consistency.error)
-    decreases x
-    requires x >= 0
-{
-    x == 0 ? 0 : f(x-1) + f(x)
-}
-
-method m(x: Int)
-    //:: ExpectedOutput(consistency.error)
-    decreases x
-{
-    var y: Int := x
-    while (y >= 0)
-    //:: ExpectedOutput(consistency.error)
-        decreases y
-    {
-        y := y-1
-    }
-
-    m(y)
-}
\ No newline at end of file

From f2fb201b57fe825c9b09d9fbdfb0f347c7cd7c32 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Tue, 18 Jul 2023 16:42:52 +0200
Subject: [PATCH 04/61] Fix typo

Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>
---
 src/main/scala/viper/silver/frontend/ViperPAstProvider.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala
index 8d8757cce..8acc71924 100644
--- a/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala
+++ b/src/main/scala/viper/silver/frontend/ViperPAstProvider.scala
@@ -57,7 +57,7 @@ class ViperPAstProvider(override val reporter: Reporter,
     override def reporter: Reporter = rep
   }
 
-  // All phases after sematic analysis omitted
+  // All phases after semantic analysis omitted
   override val phases: Seq[Phase] = Seq(Parsing, SemanticAnalysis)
 
   override def result: VerificationResult = {

From d38b2a486b8b5d5c041d9b7b72cf1d0a231a4779 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 20 Jul 2023 12:23:25 +0200
Subject: [PATCH 05/61] Emit warning if well-foundedness functions are
 constrained by incorrectly-named domain

---
 .../termination/TerminationPlugin.scala       | 53 ++++++++++++++++++-
 1 file changed, 52 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 61a0ae256..ca17ad5e9 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -19,7 +19,7 @@ import fastparse._
 import viper.silver.frontend.{DefaultStates, ViperPAstProvider}
 import viper.silver.logger.SilentLogger
 import viper.silver.parser.FastParserCompanion.whitespace
-import viper.silver.reporter.{Entity, NoopReporter}
+import viper.silver.reporter.{Entity, NoopReporter, WarningsDuringTypechecking}
 
 import scala.annotation.unused
 
@@ -113,6 +113,45 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     newProgram
   }
 
+  private def constrainsWellfoundednessUnexpectedly(ax: PAxiom, wfTypeName: Option[String]): Seq[PType] = {
+
+    def isWellFoundedFunctionCall(c: PCall): Boolean = {
+      if (!c.isDomainFunction)
+        return false
+      if (!(c.idnuse.name == "decreases" || c.idnuse.name == "bounded"))
+        return false
+      c.function match {
+        case df: PDomainFunction => df.domainName.name == "WellFoundedOrder"
+        case _ => false
+      }
+    }
+
+    def isNotExpectedConstrainedType(t: PType): Boolean = {
+      if (!t.isValidOrUndeclared)
+        return false
+      if (wfTypeName.isEmpty)
+        return true
+      val typeName = t match {
+        case PPrimitiv("Perm") => "Rational"
+        case PPrimitiv(n) => n
+        case PSeqType(_) => "Seq"
+        case PSetType(_) => "Set"
+        case PMultisetType(_) => "MultiSet"
+        case PMapType(_, _) => "Map"
+        case PDomainType(d, _) if d.name == "PredicateInstance" => "PredicateInstances"
+        case PDomainType(d, _) => d.name
+      }
+      !wfTypeName.contains(typeName)
+    }
+
+    ax.exp.shallowCollect{
+      case c: PCall if isWellFoundedFunctionCall(c) && c.domainSubstitution.isDefined &&
+        c.domainSubstitution.get.contains("T") &&
+        isNotExpectedConstrainedType(c.domainSubstitution.get.get("T").get) =>
+        c.domainSubstitution.get.get("T").get
+    }
+  }
+
   override def beforeTranslate(input: PProgram): PProgram = {
     val allClauseTypes: Set[Any] = decreasesClauses.flatMap{
       case PDecreasesTuple(Seq(), _) => Seq(())
@@ -124,6 +163,18 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     }.toSet
     val presentDomains = input.domains.map(_.idndef.name).toSet
 
+    // Check if the program contains any domains that define decreasing and bounded functions that do *not* have the expected names.
+    for (d <- input.domains) {
+      val name = d.idndef.name
+      val typeName = if (name.endsWith("WellFoundedOrder"))
+        Some(name.substring(0, name.length - 16))
+      else
+        None
+      val wronglyConstrainedTypes = d.axioms.flatMap(a => constrainsWellfoundednessUnexpectedly(a, typeName))
+      reporter.report(WarningsDuringTypechecking(wronglyConstrainedTypes.map(t =>
+        TypecheckerWarning(s"Domain ${d.idndef.name} constrains well-foundedness functions for type ${t} and should be named <Type>WellFoundedOrder instead.", d.pos._1))))
+    }
+
     val importStmts = allClauseTypes flatMap {
       case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import <decreases/int.vpr>")
       case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import <decreases/ref.vpr>")

From 91fc42e9fc7df30101b6e55ea5c4769f7db1fea4 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 20 Jul 2023 14:20:14 +0200
Subject: [PATCH 06/61] Deprecating rational well founded order, adding perm
 replacement, adapting autoimport and warning code

---
 src/main/resources/import/decreases/all.vpr   |  2 +-
 src/main/resources/import/decreases/perm.vpr  | 16 ++++++++++++++
 .../termination/TerminationPlugin.scala       | 22 +++++++++----------
 3 files changed, 28 insertions(+), 12 deletions(-)
 create mode 100644 src/main/resources/import/decreases/perm.vpr

diff --git a/src/main/resources/import/decreases/all.vpr b/src/main/resources/import/decreases/all.vpr
index dc6debd40..f3d471de5 100644
--- a/src/main/resources/import/decreases/all.vpr
+++ b/src/main/resources/import/decreases/all.vpr
@@ -5,7 +5,7 @@ import "bool.vpr"
 import "int.vpr"
 import "multiset.vpr"
 import "predicate_instance.vpr"
-import "rational.vpr"
+import "perm.vpr"
 import "ref.vpr"
 import "seq.vpr"
 import "set.vpr"
\ No newline at end of file
diff --git a/src/main/resources/import/decreases/perm.vpr b/src/main/resources/import/decreases/perm.vpr
new file mode 100644
index 000000000..050729145
--- /dev/null
+++ b/src/main/resources/import/decreases/perm.vpr
@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import "declaration.vpr"
+
+domain PermWellFoundedOrder{
+	//Rationals
+    axiom rational_ax_dec{
+        forall int1: Perm, int2: Perm :: {decreasing(int1, int2)}
+            (int1 <= int2 - 1/1) ==> decreasing(int1, int2)
+    }
+    axiom rational_ax_bound{
+        forall int1: Perm :: {bounded(int1)}
+            int1 >= 0/1 ==> bounded(int1)
+    }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index ca17ad5e9..a03f9ca01 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -131,17 +131,17 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
         return false
       if (wfTypeName.isEmpty)
         return true
-      val typeName = t match {
-        case PPrimitiv("Perm") => "Rational"
-        case PPrimitiv(n) => n
-        case PSeqType(_) => "Seq"
-        case PSetType(_) => "Set"
-        case PMultisetType(_) => "MultiSet"
-        case PMapType(_, _) => "Map"
-        case PDomainType(d, _) if d.name == "PredicateInstance" => "PredicateInstances"
-        case PDomainType(d, _) => d.name
+      val typeNames = t match {
+        case PPrimitiv("Perm") => Seq("Rational", "Perm")
+        case PPrimitiv(n) => Seq(n)
+        case PSeqType(_) => Seq("Seq")
+        case PSetType(_) => Seq("Set")
+        case PMultisetType(_) => Seq("MultiSet")
+        case PMapType(_, _) => Seq("Map")
+        case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances")
+        case PDomainType(d, _) => Seq(d.name)
       }
-      !wfTypeName.contains(typeName)
+      !typeNames.exists(tn => wfTypeName.contains(tn))
     }
 
     ax.exp.shallowCollect{
@@ -179,7 +179,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       case TypeHelper.Int if !presentDomains.contains("IntWellFoundedOrder") => Some("import <decreases/int.vpr>")
       case TypeHelper.Ref if !presentDomains.contains("RefWellFoundedOrder") => Some("import <decreases/ref.vpr>")
       case TypeHelper.Bool if !presentDomains.contains("BoolWellFoundedOrder") => Some("import <decreases/bool.vpr>")
-      case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") => Some("import <decreases/rational.vpr>")
+      case TypeHelper.Perm if !presentDomains.contains("RationalWellFoundedOrder") && !presentDomains.contains("PermWellFoundedOrder") => Some("import <decreases/perm.vpr>")
       case PMultisetType(_) if !presentDomains.contains("MultiSetWellFoundedOrder") => Some("import <decreases/multiset.vpr>")
       case PSeqType(_) if !presentDomains.contains("SeqWellFoundedOrder") => Some("import <decreases/seq.vpr>")
       case PSetType(_) if !presentDomains.contains("SetWellFoundedOrder") => Some("import <decreases/set.vpr>")

From 4f57dc7ebf6c31a4a0ca75ada24099ebd7692621 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Wed, 2 Aug 2023 03:29:10 +0200
Subject: [PATCH 07/61] Release notes for 2023.7

---
 ReleaseNotes.md | 77 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

diff --git a/ReleaseNotes.md b/ReleaseNotes.md
index c3390040c..b46af1909 100644
--- a/ReleaseNotes.md
+++ b/ReleaseNotes.md
@@ -1,3 +1,80 @@
+## Release 2023.7
+
+**Date 31/07/23**
+
+### Changes in Viper Language
+
+- Improved language flexibility ([Silver#685](https://github.com/viperproject/silver/pull/685)): The syntax of declarations and assignments is now more permissive, allowing, for example, multiple declarations at once:
+  ```
+  field n: Ref, m: Ref  // Declare multiple fields at once
+  var a: Ref, b: Ref, c: Int  // Declare multiple locals at once
+  ```
+  Additionally, method calls and new statements can now have fields or newly-declared local variables on their left hand side:
+  ```
+  var f: Ref := new(n)                   // Declare and initialise locals with `new`
+  a, f.n := get_refs()                   // Assign to field from method call
+  f.n := new(n)                          // Assign to field with `new`
+  ```
+  The Viper AST remains unchanged; the newly-supported syntax is desugared into equivalent code that uses the existing Viper AST.
+- Annotations ([Silver#666](https://github.com/viperproject/silver/pull/666)): The Viper language now has support for annotations on statements, expressions, and top-level declarations. The syntax for an annotation is ``@key("value", "value2", ...)``, i.e., they have a key which is preceded by an ``@`` sign and a sequence of values written as comma-separated string literals. A single expression/statement/declaration can have multiple annotations. If there are two annotations of the same key, their value sequences are concatenated. In the AST, annotations are represented in the ``info`` field of the annotated AST node using an ``AnnotationInfo`` object.
+  Currently, there are two supported annotations: ``@weight("n")`` on quantifiers, where ``n`` is a positive integer, sets the weight of the quantifier in the SMT solver.
+  The second annotation is exclusive to the Symbolic Execution backend (see below).
+  Unknown annotations are ignored.
+- Domain axioms may now refer to non-domain functions that do not have any preconditions ([Silver#698](https://github.com/viperproject/silver/pull/698)).
+- Support for chained comparisons ([Silver#713](https://github.com/viperproject/silver/pull/713)): expressions like ``e1 < e2 <= e3 > e4`` can now be parsed and will be desugared to ``(e1 < e2) && (e2 <= e3) && (e3 > e4)``. The AST nodes for comparison operations remain unchanged.
+- Two important changes in the termination plugin:
+  - The termination plugin now enforces that functions that refer to themselves (or to other functions that call the original function in a mutually-recursive way) in their own postconditions have a ``decreases`` clause ([Silver#711](https://github.com/viperproject/silver/pull/711)). That is, for such functions, one must either prove termination using a ``decreases`` clause, or explicitly state that termination should be assumed by writing ``decreases *``.
+    This change addresses frequent issues where users wrote functions that are not well-defined using such postconditions and subsequently reported seemingly unsound behavior (e.g., ([Silver#525](https://github.com/viperproject/silver/issues/525)) and ([Silver#668](https://github.com/viperproject/silver/issues/668))).
+  - The termination plugin now automatically imports the default definitions of well-founded orders if ``decreases``-clauses are used but no such definitions are present in the program ([Silver#710](https://github.com/viperproject/silver/pull/710)). That is, it is not longer necessary (but still possible) to write an import statement like ``import <decreases/int.vpr>`` when using a termination measure of type integer.
+- The ``Rational`` type, an alias for ``Perm``, is deprecated. Viper issues a warning whenever the type is used.
+
+### Other Viper-level Improvements
+
+- Improved error messages for parse errors ([Silver#702](https://github.com/viperproject/silver/pull/702)) and type errors (([Silver#684](https://github.com/viperproject/silver/pull/684)), ([Silver#724](https://github.com/viperproject/silver/pull/724)))
+- Fixed parsing and pretty-printing of scopes ([Silver#704](https://github.com/viperproject/silver/pull/704)), which were previously ommitted under some circumstances by both the pretty-printer and the parser, which could make otherwise valid Viper code invalid. 
+- Introduced caching to improve performance of common lookups on the AST (([Silver#659](https://github.com/viperproject/silver/pull/659)) and ([Silver#719](https://github.com/viperproject/silver/pull/719)))
+- Viper now reports inferred quantifiers using a ``QuantifierInstantiationsMessage`` ([Silver#653](https://github.com/viperproject/silver/pull/653))
+- Introduced various new consistency checks for invalid code that used to crash the backends or lead to unexpected behavior:
+  - ``perm``-expressions are no longer allowed in function postconditions ([Silver#681](https://github.com/viperproject/silver/pull/681))
+  - ``wildcard`` is no longer allowed as part of compound expressions ([Silver#700](https://github.com/viperproject/silver/pull/700))
+  - empty ADTs are rejected ([Silver#696](https://github.com/viperproject/silver/pull/696))
+  - predicate argument expressions must be pure ([Silver#721](https://github.com/viperproject/silver/pull/721))
+- Labelled ``old``-expressions may now be used as triggers ([Silver#695](https://github.com/viperproject/silver/pull/695))
+- Various small fixes for crashes or other incorrect behavior.
+
+### Backend-specific Upgrades/Changes
+
+#### Symbolic Execution Backend (Silicon)
+
+- The previously experimental mode ``--moreCompleteExhale`` is no longer experimental, but is now a supported mode that performs exhales and heap lookups in a way that is usually more complete (but possibly slower). However, Silicon's previous exhale mode remains the default. ([Silicon#682](https://github.com/viperproject/silicon/pull/682))
+  - The new flag ``--exhaleMode=n``, where ``n`` is 0, 1, or 2, can now be used to select the exhale mode. 0 is the default, 1 is the previous ``moreCompleteExhale`` mode.
+  - The new ``exhaleMode`` 2 uses the default exhale mode 0 throughout the program, until it encounters a verification error. When it does, it retries proving the failing assertion using the (more complete) mode 1. Since mode 0 is usually faster than mode 1, mode 2 often results in the best mix of performance and completeness.
+  - Additionally, one can now override the exhale mode selected via command line for individual methods using an annotation ``@exhaleMode("n")`` on the method ([Silicon#724](https://github.com/viperproject/silicon/pull/724))
+- Via the option ``--prover=Z3-API``, Silicon can now use Z3 as a library via its Java API (([Silicon#633](https://github.com/viperproject/silicon/pull/633)) and ([Silicon#692](https://github.com/viperproject/silicon/pull/692))). Note that this requires a native version of ``libz3java`` to be present on the path Java uses to look for native libraries (which can be set, e.g., via the environment variable``LD_LIBRARY_PATH`` on Linux or ``DYLD_LIBRARY_PATH`` on MacOS).
+  Depending on the OS and the Viper program, this option can lead to a significant speedup.
+- Silicon now emits warnings in cases where it cannot use the triggers specified by the user ([Silicon#687](https://github.com/viperproject/silicon/pull/687))
+- ``old``-expressions in triggers are now interpreted correctly ([Silicon#710](https://github.com/viperproject/silicon/pull/710)); previously, they were sometimes ignored.
+- Changed default options used for Z3; the new options have similar performance and completeness characteristics with the supported Z3 version 4.8.7, but perform better with newer versions (tested in particular with 4.12.1) ([Silicon#694](https://github.com/viperproject/silicon/pull/694))
+- Silicon now longer creates a ``tmp`` directory containing ``.smt2`` files that log its prover interactions by default ([Silicon#709](https://github.com/viperproject/silicon/pull/709)). The flag ``--disableTempDirectory`` no longer exists. Instead, one can use the new flag ``--enableTempDirectory`` or the flag ``--proverLogFile``. 
+- Improved heuristics for handling of quantified permissions, which improves performance in some cases ([Silicon#704](https://github.com/viperproject/silicon/pull/704))
+- Fixed some incorrect (too short) timeouts, which could lead to unstable verification results in some cases ([Silicon#705](https://github.com/viperproject/silicon/pull/705))
+- Added a new command line flag ``--reportReasonUnknown``, which instructs Silicon to report the reason the SMT solver names for not being able to prove a property (per error)  ([Silicon#701](https://github.com/viperproject/silicon/pull/701)). This flag can be useful to find out whether an error occurred due to non-linear arithmetic or timeouts.
+- Fixed four unsoundnesses:
+  - Incorrect handling of ``old``-expressions in postconditions of methods called inside a ``package`` statement ([Silicon#699](https://github.com/viperproject/silicon/pull/699))
+  - Incorrect handling of ``fold`` statements for predicates that are used inside a quantified permission in the current method ([Silicon#696](https://github.com/viperproject/silicon/pull/696))
+  - Incorrect behavior for quantifiers whose bodies have unreachable branches ([Silicon#690](https://github.com/viperproject/silicon/pull/690))
+  - Exhale mode 1 now correctly checks permission amounts in function preconditions ([Silicon#682](https://github.com/viperproject/silicon/pull/682))
+- Fixed and generalized the experimental mode ``--conditionalizePermissions``, which avoids branching on conditional permission assertions (e.g., ``b ==> acc(x.f)``) by rewriting them to unconditional assertions with conditional permission amounts (e.g., ``acc(x.f, b ? write : none)`` whenever possible ([Silicon#685](https://github.com/viperproject/silicon/pull/685)). For programs with many branches, this option can improve performance.
+- Resource triggers on existentials now work correctly ([Silicon#679](https://github.com/viperproject/silicon/pull/679))
+- More complete computation of function footprints ([Silicon#684](https://github.com/viperproject/silicon/pull/684))
+- Various smaller bug fixes
+
+#### Verification Condition Generation Backend (Carbon)
+
+- Improved encoding of well-definedness checks for field accesses and permission division ([Carbon#451](https://github.com/viperproject/carbon/pull/451)). As a result, Carbon now emits well-definedness errors in the expected order in some cases where this was previously not the case.
+- Improved encoding of definedness checks during exhale ([Carbon#457](https://github.com/viperproject/carbon/pull/457)). This fixed both possible unsoundness and incompleteness issues.
+- Using stdin instead of a temporary file to communicate with Boogie ([Carbon#456](https://github.com/viperproject/carbon/pull/456))
+
 ## Release 2023.1
 
 **Date 25/01/23**

From c4b489119ba2659a35ce01235edae56cf7ac0bf7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Thu, 3 Aug 2023 14:49:15 +0200
Subject: [PATCH 08/61] Fixing typo Gaurav found

---
 ReleaseNotes.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ReleaseNotes.md b/ReleaseNotes.md
index b46af1909..22785423f 100644
--- a/ReleaseNotes.md
+++ b/ReleaseNotes.md
@@ -55,7 +55,7 @@
 - Silicon now emits warnings in cases where it cannot use the triggers specified by the user ([Silicon#687](https://github.com/viperproject/silicon/pull/687))
 - ``old``-expressions in triggers are now interpreted correctly ([Silicon#710](https://github.com/viperproject/silicon/pull/710)); previously, they were sometimes ignored.
 - Changed default options used for Z3; the new options have similar performance and completeness characteristics with the supported Z3 version 4.8.7, but perform better with newer versions (tested in particular with 4.12.1) ([Silicon#694](https://github.com/viperproject/silicon/pull/694))
-- Silicon now longer creates a ``tmp`` directory containing ``.smt2`` files that log its prover interactions by default ([Silicon#709](https://github.com/viperproject/silicon/pull/709)). The flag ``--disableTempDirectory`` no longer exists. Instead, one can use the new flag ``--enableTempDirectory`` or the flag ``--proverLogFile``. 
+- Silicon no longer creates a ``tmp`` directory containing ``.smt2`` files that log its prover interactions by default ([Silicon#709](https://github.com/viperproject/silicon/pull/709)). The flag ``--disableTempDirectory`` no longer exists. Instead, one can use the new flag ``--enableTempDirectory`` or the flag ``--proverLogFile``. 
 - Improved heuristics for handling of quantified permissions, which improves performance in some cases ([Silicon#704](https://github.com/viperproject/silicon/pull/704))
 - Fixed some incorrect (too short) timeouts, which could lead to unstable verification results in some cases ([Silicon#705](https://github.com/viperproject/silicon/pull/705))
 - Added a new command line flag ``--reportReasonUnknown``, which instructs Silicon to report the reason the SMT solver names for not being able to prove a property (per error)  ([Silicon#701](https://github.com/viperproject/silicon/pull/701)). This flag can be useful to find out whether an error occurred due to non-linear arithmetic or timeouts.

From 258ed3bf9cb318a7d4a72a9218773798f8e52879 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 4 Aug 2023 16:03:55 +0200
Subject: [PATCH 09/61] Do not performa new checks and imports if the
 termination plugin is deactivated

---
 .../termination/TerminationPlugin.scala       | 43 +++++++++++--------
 1 file changed, 24 insertions(+), 19 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index a03f9ca01..2c9d2427e 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -153,6 +153,9 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   }
 
   override def beforeTranslate(input: PProgram): PProgram = {
+    if (deactivated)
+      return input
+
     val allClauseTypes: Set[Any] = decreasesClauses.flatMap{
       case PDecreasesTuple(Seq(), _) => Seq(())
       case PDecreasesTuple(exps, _) => exps.map(e => e.typ match {
@@ -240,27 +243,29 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   override def beforeVerify(input: Program): Program = {
     // Prevent potentially unsafe (mutually) recursive function calls in function postcondtions
     // for all functions that don't have a decreases clause
-    lazy val cycles = Functions.findFunctionCyclesViaOptimized(input, func => func.body.toSeq)
-    for (f <- input.functions) {
-      val hasDecreasesClause = (f.pres ++ f.posts).exists(p => p.shallowCollect {
-        case dc: DecreasesClause => dc
-      }.nonEmpty)
-      if (!hasDecreasesClause) {
-        val funcCycles = cycles.get(f)
-        val problematicFuncApps = f.posts.flatMap(p => p.shallowCollect {
-          case fa: FuncApp if fa.func(input) == f => fa
-          case fa: FuncApp if funcCycles.isDefined && funcCycles.get.contains(fa.func(input)) => fa
-        }).toSet
-        for (fa <- problematicFuncApps) {
-          val calledFunc = fa.func(input)
-          if (calledFunc == f) {
-            if (fa.args == f.formalArgs.map(_.localVar)) {
-              reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Use \"result\" instead to refer to the result of the function.", fa.pos))
+    if (!deactivated) {
+      lazy val cycles = Functions.findFunctionCyclesViaOptimized(input, func => func.body.toSeq)
+      for (f <- input.functions) {
+        val hasDecreasesClause = (f.pres ++ f.posts).exists(p => p.shallowCollect {
+          case dc: DecreasesClause => dc
+        }.nonEmpty)
+        if (!hasDecreasesClause) {
+          val funcCycles = cycles.get(f)
+          val problematicFuncApps = f.posts.flatMap(p => p.shallowCollect {
+            case fa: FuncApp if fa.func(input) == f => fa
+            case fa: FuncApp if funcCycles.isDefined && funcCycles.get.contains(fa.func(input)) => fa
+          }).toSet
+          for (fa <- problematicFuncApps) {
+            val calledFunc = fa.func(input)
+            if (calledFunc == f) {
+              if (fa.args == f.formalArgs.map(_.localVar)) {
+                reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Use \"result\" instead to refer to the result of the function.", fa.pos))
+              } else {
+                reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
+              }
             } else {
-              reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
+              reportError(ConsistencyError(s"Function ${f.name} has a call to mutually-recursive function ${calledFunc.name} in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
             }
-          } else {
-            reportError(ConsistencyError(s"Function ${f.name} has a call to mutually-recursive function ${calledFunc.name} in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
           }
         }
       }

From c1a1a4d1a05f3ff21e6f088572ba499ac87772f3 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 14 Aug 2023 12:49:24 +0200
Subject: [PATCH 10/61] WIP

---
 .../silver/frontend/SilFrontEndConfig.scala   |  7 ++++
 .../viper/silver/frontend/SilFrontend.scala   | 15 ++++++++
 .../silver/frontend/ViperFrontendAPI.scala    | 38 +++++++++++++++++++
 3 files changed, 60 insertions(+)
 create mode 100644 src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala

diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
index 62fa07f4f..cff594043 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
@@ -82,6 +82,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = true
   )
 
+  val disableDefaultPlugins = opt[Boolean]("disableDefaultPlugins",
+    descr = "Deactivate all default plugins.",
+    default = Some(false),
+    noshort = true,
+    hidden = true
+  )
+
   val plugin = opt[String]("plugin",
     descr = "Load plugin(s) with given class name(s). Several plugins can be separated by ':'. " +
       "The fully qualified class name of the plugin should be specified.",
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index f1e336091..8bac404cf 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -52,6 +52,21 @@ trait SilFrontend extends DefaultFrontend {
     }
   }
 
+  def resetPlugins(): Unit = {
+    val pluginsArg: Option[String] = if (_config != null) {
+      // concat defined plugins and default plugins
+      val list = _config.plugin.toOption ++ (if (_config.disableDefaultPlugins()) Seq() else defaultPlugins)
+      if (list.isEmpty) {
+        None
+      } else {
+        Some(list.mkString(":"))
+      }
+    } else {
+      None
+    }
+    _plugins = SilverPluginManager(pluginsArg)(reporter, logger, _config, fp)
+  }
+
   /**
    * Create the verifier. The full command is parsed for debugging purposes only,
    * since the command line arguments will be passed later on via
diff --git a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
new file mode 100644
index 000000000..03c9a1447
--- /dev/null
+++ b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
@@ -0,0 +1,38 @@
+package viper.silver.frontend
+
+import viper.silver.ast.Program
+import viper.silver.verifier.VerificationResult
+
+import java.nio.file.Paths
+
+trait ViperFrontendAPI extends SilFrontend {
+
+  private var initialized = false
+  override val phases: Seq[Phase] = Seq(ConsistencyCheck, Verification)
+  val dummyInputFilename = "dummy-file-to-prevent-cli-parser-from-complaining-about-missing-file-name.silver"
+
+  def initialize(args: Seq[String]): Unit = {
+    // create verifier
+    // parse args on frontend, set on verifier
+    val v = createVerifier(args.mkString(" "))
+    setVerifier(v)
+    _verifier = Some(v)
+    parseCommandLine(args :+ "--ignoreFile" :+ dummyInputFilename)
+    resetPlugins()
+    initialized = true
+  }
+
+  protected def setStartingState() = {
+    _state = DefaultStates.ConsistencyCheck
+  }
+
+  def verify(p: Program): VerificationResult = {
+    if (!initialized)
+      println("Not initialized")
+    setStartingState()
+    _program = Some(p)
+    runAllPhases()
+    result
+  }
+
+}

From e55f4e8dbcb4cd541137e108c3a5dcd86c34881e Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 14 Aug 2023 13:02:42 +0200
Subject: [PATCH 11/61] Adding test for Silicon issue #740

---
 .../resources/all/issues/silicon/0740.vpr     | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0740.vpr

diff --git a/src/test/resources/all/issues/silicon/0740.vpr b/src/test/resources/all/issues/silicon/0740.vpr
new file mode 100644
index 000000000..3449fdaed
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0740.vpr
@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Bool
+
+method fails(a: Bool)
+{
+    var curr: Ref := null
+
+    while (curr != null)
+        invariant curr != null ==> acc(curr.f)
+    {
+        refute false
+        curr := null
+    }
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
\ No newline at end of file

From d78442093c12416190dd13cf91573d7b8a111ebb Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 14 Aug 2023 14:07:11 +0200
Subject: [PATCH 12/61] Some comments

---
 .../silver/frontend/ViperFrontendAPI.scala    | 25 ++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
index 03c9a1447..cb4585d76 100644
--- a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
+++ b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
@@ -5,6 +5,18 @@ import viper.silver.verifier.VerificationResult
 
 import java.nio.file.Paths
 
+/**
+  * Trait that can be mixed into SilFrontends to make them easily usable by actual Viper frontends that do not use
+  * Viper's parser, type checker, etc., but instead directly consistency-check and verify a Viper AST.
+  * Compared to working directly with an instance of [[viper.silver.verifier.Verifier]], SilFrontend manages plugins
+  * automatically.
+  * To use it:
+  * - create an instance f of a specific SilFrontend with ViperFrontendAPI mixed in
+  * - call f.initialize(args), where args are the command line arguments without any file name.
+  * - (potentially repeatedly) call f.verify(p), where p is the program to verify
+  * Plugin usage must be managed via command line arguments.
+  * Existing implementations are SiliconFrontendAPI and CarbonFrontendAPI
+  */
 trait ViperFrontendAPI extends SilFrontend {
 
   private var initialized = false
@@ -28,7 +40,7 @@ trait ViperFrontendAPI extends SilFrontend {
 
   def verify(p: Program): VerificationResult = {
     if (!initialized)
-      println("Not initialized")
+      throw new IllegalStateException("Not initialized")
     setStartingState()
     _program = Some(p)
     runAllPhases()
@@ -36,3 +48,14 @@ trait ViperFrontendAPI extends SilFrontend {
   }
 
 }
+
+/**
+  * Version of ViperFrontendAPI that skips the consistency check phase.
+  */
+trait MinimalViperFrontendAPI extends ViperFrontendAPI {
+  override val phases: Seq[Phase] = Seq(Verification)
+
+  override protected def setStartingState() = {
+    _state = DefaultStates.ConsistencyCheck
+  }
+}

From bfdf70b13df618129577bfcd5f93d7bd0eed2493 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 14 Aug 2023 19:05:38 +0200
Subject: [PATCH 13/61] Added missing case (fixes Silicon issue #742)

---
 .../silver/plugin/standard/termination/TerminationPlugin.scala   | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 2c9d2427e..85ed54c2d 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -140,6 +140,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
         case PMapType(_, _) => Seq("Map")
         case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances")
         case PDomainType(d, _) => Seq(d.name)
+        case gt: PGenericType => Seq(gt.genericName)
       }
       !typeNames.exists(tn => wfTypeName.contains(tn))
     }

From 948b7e9265b5a245ff6e8f16993d26fc34ea99d9 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 14 Aug 2023 19:51:00 +0200
Subject: [PATCH 14/61] Added test case

---
 .../resources/all/issues/silicon/0742.vpr     | 28 +++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0742.vpr

diff --git a/src/test/resources/all/issues/silicon/0742.vpr b/src/test/resources/all/issues/silicon/0742.vpr
new file mode 100644
index 000000000..767bbd458
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0742.vpr
@@ -0,0 +1,28 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/all.vpr>
+
+domain ListWellFoundedOrder[T] {
+
+
+  axiom {
+    forall y : List[T] :: {bounded(y)} bounded(y)
+  }
+
+
+  axiom {
+    forall xs : List[T] , y : T ::
+      decreasing(xs, Cons(y, xs))
+  }
+
+  axiom {
+    forall xs : List[T], ys : List[T], zs : List[T] :: {decreasing(xs, ys), decreasing(ys, zs)}
+      decreasing(xs, ys) && decreasing(ys, zs) ==> decreasing(xs, zs)
+  }
+}
+
+adt List[T] {
+  Nil()
+  Cons(value : T, tail : List[T])
+}
\ No newline at end of file

From afaf4523a8429873c4f160713a22764162b12b21 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 15 Aug 2023 00:31:17 +0200
Subject: [PATCH 15/61] Removed duplicated code

---
 src/main/scala/viper/silver/frontend/SilFrontend.scala | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index 8bac404cf..a2ee386f0 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -199,13 +199,7 @@ trait SilFrontend extends DefaultFrontend {
     super.reset(input)
 
     if(_config != null) {
-
-      // concat defined plugins and default plugins
-      val pluginsArg: Option[String] = {
-        val list = _config.plugin.toOption ++ defaultPlugins
-        if (list.isEmpty) { None } else { Some(list.mkString(":")) }
-      }
-      _plugins = SilverPluginManager(pluginsArg)(reporter, logger, _config, fp)
+      resetPlugins()
     }
   }
 

From d52e42faec49614fc5e280d7960b15f8924da1de Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 16 Aug 2023 21:52:10 +0200
Subject: [PATCH 16/61] Added stop method to API, fixed random CE extraction
 issue

---
 .../scala/viper/silver/frontend/ViperFrontendAPI.scala    | 8 +++++++-
 .../scala/viper/silver/verifier/VerificationError.scala   | 2 +-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
index cb4585d76..2e2517364 100644
--- a/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
+++ b/src/main/scala/viper/silver/frontend/ViperFrontendAPI.scala
@@ -3,7 +3,6 @@ package viper.silver.frontend
 import viper.silver.ast.Program
 import viper.silver.verifier.VerificationResult
 
-import java.nio.file.Paths
 
 /**
   * Trait that can be mixed into SilFrontends to make them easily usable by actual Viper frontends that do not use
@@ -14,6 +13,7 @@ import java.nio.file.Paths
   * - create an instance f of a specific SilFrontend with ViperFrontendAPI mixed in
   * - call f.initialize(args), where args are the command line arguments without any file name.
   * - (potentially repeatedly) call f.verify(p), where p is the program to verify
+  * - call f.stop() when done
   * Plugin usage must be managed via command line arguments.
   * Existing implementations are SiliconFrontendAPI and CarbonFrontendAPI
   */
@@ -47,6 +47,12 @@ trait ViperFrontendAPI extends SilFrontend {
     result
   }
 
+  def stop(): Unit = {
+    if (!initialized)
+      throw new IllegalStateException("Not initialized")
+    _verifier.foreach(_.stop())
+  }
+
 }
 
 /**
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 16180457f..67c0c66e0 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -93,7 +93,7 @@ case class MapEntry(options: Map[Seq[ValueEntry], ValueEntry], default: ValueEnt
         val indices = args.map(_.get._1)
         // We expect the arguments in the order 0, 1, ..., n-1; if we get something else, reject.
         // TODO: Find out if this order is always guaranteed,
-        if (indices != (0 until indices.size))
+        if (indices != (0 until indices.size).map(_.toString))
           None
         else
           Some(args.map(_.get._2))

From 22314c8068ec82b8cdff02f3fbc7009a3d2dbccb Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Thu, 17 Aug 2023 19:12:48 +0200
Subject: [PATCH 17/61] Update ReleaseNotes.md

---
 ReleaseNotes.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/ReleaseNotes.md b/ReleaseNotes.md
index 22785423f..1a3386299 100644
--- a/ReleaseNotes.md
+++ b/ReleaseNotes.md
@@ -28,6 +28,10 @@
   - The termination plugin now automatically imports the default definitions of well-founded orders if ``decreases``-clauses are used but no such definitions are present in the program ([Silver#710](https://github.com/viperproject/silver/pull/710)). That is, it is not longer necessary (but still possible) to write an import statement like ``import <decreases/int.vpr>`` when using a termination measure of type integer.
 - The ``Rational`` type, an alias for ``Perm``, is deprecated. Viper issues a warning whenever the type is used.
 
+### Viper API Changes
+
+- Introduced a new API for frontends to interact with Viper ([Silver#732](https://github.com/viperproject/silver/pull/732)). Frontends can create instances of ``ViperFrontendAPI``  and interact exclusively through those (instead of instances of ``Verifier`` or ``SilFrontend``), which saves some boilerplate code and lets Viper manage plugins. 
+
 ### Other Viper-level Improvements
 
 - Improved error messages for parse errors ([Silver#702](https://github.com/viperproject/silver/pull/702)) and type errors (([Silver#684](https://github.com/viperproject/silver/pull/684)), ([Silver#724](https://github.com/viperproject/silver/pull/724)))
@@ -59,10 +63,11 @@
 - Improved heuristics for handling of quantified permissions, which improves performance in some cases ([Silicon#704](https://github.com/viperproject/silicon/pull/704))
 - Fixed some incorrect (too short) timeouts, which could lead to unstable verification results in some cases ([Silicon#705](https://github.com/viperproject/silicon/pull/705))
 - Added a new command line flag ``--reportReasonUnknown``, which instructs Silicon to report the reason the SMT solver names for not being able to prove a property (per error)  ([Silicon#701](https://github.com/viperproject/silicon/pull/701)). This flag can be useful to find out whether an error occurred due to non-linear arithmetic or timeouts.
-- Fixed four unsoundnesses:
+- Fixed five unsoundnesses:
   - Incorrect handling of ``old``-expressions in postconditions of methods called inside a ``package`` statement ([Silicon#699](https://github.com/viperproject/silicon/pull/699))
   - Incorrect handling of ``fold`` statements for predicates that are used inside a quantified permission in the current method ([Silicon#696](https://github.com/viperproject/silicon/pull/696))
   - Incorrect behavior for quantifiers whose bodies have unreachable branches ([Silicon#690](https://github.com/viperproject/silicon/pull/690))
+  - Incorrectly terminating verification after using a ``refute`` ([Silicon#741](https://github.com/viperproject/silicon/pull/741))
   - Exhale mode 1 now correctly checks permission amounts in function preconditions ([Silicon#682](https://github.com/viperproject/silicon/pull/682))
 - Fixed and generalized the experimental mode ``--conditionalizePermissions``, which avoids branching on conditional permission assertions (e.g., ``b ==> acc(x.f)``) by rewriting them to unconditional assertions with conditional permission amounts (e.g., ``acc(x.f, b ? write : none)`` whenever possible ([Silicon#685](https://github.com/viperproject/silicon/pull/685)). For programs with many branches, this option can improve performance.
 - Resource triggers on existentials now work correctly ([Silicon#679](https://github.com/viperproject/silicon/pull/679))

From c72b49699c65fc693b34cc71f5155f35bac697b4 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sat, 19 Aug 2023 23:24:52 +0200
Subject: [PATCH 18/61] Fixing refute plugin for nodes with several info nodes

---
 .../silver/plugin/standard/refute/RefutePlugin.scala  | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index 831ba54ad..131fb58cc 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -81,12 +81,12 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
     val (refutesForWhichErrorOccurred, otherErrors) = input match {
       case Success => (Seq.empty, Seq.empty)
       case Failure(errors) => errors.partitionMap {
-        case AssertFailed(NodeWithInfo(RefuteInfo(r)), _, _) => Left((r, r.pos))
+        case AssertFailed(NodeWithRefuteInfo(RefuteInfo(r)), _, _) => Left((r, r.pos))
         case err => Right(err)
       }
     }
     val refutesContainedInNode = n.collect {
-      case NodeWithInfo(RefuteInfo(r)) => (r, r.pos)
+      case NodeWithRefuteInfo(RefuteInfo(r)) => (r, r.pos)
     }
     // note that we include positional information in `refutesForWhichErrorOccurred` and `refutesContainedInNode` such
     // that we do not miss errors just because the same refute statement occurs multiple times
@@ -101,6 +101,9 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
   }
 }
 
-object NodeWithInfo {
-  def unapply(node : Node) : Option[Info] = Some(node.meta._2)
+object NodeWithRefuteInfo {
+  def unapply(node : Node) : Option[RefuteInfo] = node match {
+    case i: Infoed => i.info.getUniqueInfo[RefuteInfo]
+    case _ => None
+  }
 }

From b4e6a56eea771c1462302f5f84ad3565714c776e Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sat, 19 Aug 2023 23:33:16 +0200
Subject: [PATCH 19/61] Added test

---
 src/test/resources/all/issues/silver/0735.vpr | 694 ++++++++++++++++++
 1 file changed, 694 insertions(+)
 create mode 100644 src/test/resources/all/issues/silver/0735.vpr

diff --git a/src/test/resources/all/issues/silver/0735.vpr b/src/test/resources/all/issues/silver/0735.vpr
new file mode 100644
index 000000000..2dd3d8a4f
--- /dev/null
+++ b/src/test/resources/all/issues/silver/0735.vpr
@@ -0,0 +1,694 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain PyType  {
+
+  function extends_(sub: PyType, super: PyType): Bool
+
+  function issubtype(sub: PyType, super: PyType): Bool
+
+  function isnotsubtype(sub: PyType, super: PyType): Bool
+
+  function tuple_args(t: PyType): Seq[PyType]
+
+  function typeof(obj: Ref): PyType
+
+  function get_basic(t: PyType): PyType
+
+  function union_type_1(arg_1: PyType): PyType
+
+  function union_type_2(arg_1: PyType, arg_2: PyType): PyType
+
+  function union_type_3(arg_1: PyType, arg_2: PyType, arg_3: PyType): PyType
+
+  function union_type_4(arg_1: PyType, arg_2: PyType, arg_3: PyType, arg_4: PyType): PyType
+
+  unique function object(): PyType
+
+  unique function list_basic(): PyType
+
+  function list(arg0: PyType): PyType
+
+  function list_arg(typ: PyType, index: Int): PyType
+
+  unique function set_basic(): PyType
+
+  function set(arg0: PyType): PyType
+
+  function set_arg(typ: PyType, index: Int): PyType
+
+  unique function dict_basic(): PyType
+
+  function dict(arg0: PyType, arg1: PyType): PyType
+
+  function dict_arg(typ: PyType, index: Int): PyType
+
+  unique function int(): PyType
+
+  unique function float(): PyType
+
+  unique function bool(): PyType
+
+  unique function NoneType(): PyType
+
+  unique function Exception(): PyType
+
+  unique function ConnectionRefusedError(): PyType
+
+  unique function traceback(): PyType
+
+  unique function str(): PyType
+
+  unique function bytes(): PyType
+
+  unique function tuple_basic(): PyType
+
+  function tuple(args: Seq[PyType]): PyType
+
+  function tuple_arg(typ: PyType, index: Int): PyType
+
+  unique function PSeq_basic(): PyType
+
+  function PSeq(arg0: PyType): PyType
+
+  function PSeq_arg(typ: PyType, index: Int): PyType
+
+  unique function PSet_basic(): PyType
+
+  function PSet(arg0: PyType): PyType
+
+  function PSet_arg(typ: PyType, index: Int): PyType
+
+  unique function PMultiset_basic(): PyType
+
+  function PMultiset(arg0: PyType): PyType
+
+  function PMultiset_arg(typ: PyType, index: Int): PyType
+
+  unique function slice(): PyType
+
+  unique function range_0(): PyType
+
+  unique function Iterator_basic(): PyType
+
+  function Iterator(arg0: PyType): PyType
+
+  function Iterator_arg(typ: PyType, index: Int): PyType
+
+  unique function Thread_0(): PyType
+
+  unique function LevelType(): PyType
+
+  unique function type(): PyType
+
+  unique function Place(): PyType
+
+  unique function __prim__Seq_type(): PyType
+
+  axiom issubtype_transitivity {
+    (forall sub: PyType, middle: PyType, super: PyType ::
+      { issubtype(sub, middle), issubtype(middle, super) }
+      issubtype(sub, middle) && issubtype(middle, super) ==>
+      issubtype(sub, super))
+  }
+
+  axiom issubtype_reflexivity {
+    (forall type_: PyType ::
+      { issubtype(type_, type_) }
+      issubtype(type_, type_))
+  }
+
+  axiom extends_implies_subtype {
+    (forall sub: PyType, sub2: PyType ::
+      { extends_(sub, sub2) }
+      extends_(sub, sub2) ==> issubtype(sub, sub2))
+  }
+
+  axiom null_nonetype {
+    (forall r: Ref ::
+      { typeof(r) }
+      issubtype(typeof(r), NoneType()) == (r == null))
+  }
+
+  axiom issubtype_object {
+    (forall type_: PyType ::
+      { issubtype(type_, object()) }
+      issubtype(type_, object()))
+  }
+
+  axiom issubtype_exclusion {
+    (forall sub: PyType, sub2: PyType, super: PyType ::
+      { extends_(sub, super), extends_(sub2, super) }
+      extends_(sub, super) && extends_(sub2, super) && sub != sub2 ==>
+      isnotsubtype(sub, sub2) && isnotsubtype(sub2, sub))
+  }
+
+  axiom issubtype_exclusion_2 {
+    (forall sub: PyType, super: PyType ::
+      { issubtype(sub, super) }
+      { issubtype(super, sub) }
+      issubtype(sub, super) && sub != super ==> !issubtype(super, sub))
+  }
+
+  axiom issubtype_exclusion_propagation {
+    (forall sub: PyType, middle: PyType, super: PyType ::
+      { issubtype(sub, middle), isnotsubtype(middle, super) }
+      issubtype(sub, middle) && isnotsubtype(middle, super) ==>
+      !issubtype(sub, super))
+  }
+
+  axiom tuple_arg_def {
+    (forall seq: Seq[PyType], i: Int, Z: PyType ::
+      { tuple(seq), tuple_arg(Z, i) }
+      issubtype(Z, tuple(seq)) ==> issubtype(tuple_arg(Z, i), seq[i]))
+  }
+
+  axiom tuple_args_def {
+    (forall seq: Seq[PyType], Z: PyType ::
+      { issubtype(Z, tuple(seq)) }
+      issubtype(Z, tuple(seq)) ==> |tuple_args(Z)| == |seq|)
+  }
+
+  axiom tuple_self_subtype {
+    (forall seq1: Seq[PyType], seq2: Seq[PyType] ::seq1 != seq2 &&
+      |seq1| == |seq2| &&
+      (forall i: Int ::i >= 0 && i < |seq1| ==> issubtype(seq1[i], seq2[i])) ==>
+      issubtype(tuple(seq1), tuple(seq2)))
+  }
+
+  axiom union_subtype_1 {
+    (forall arg_1: PyType, X: PyType ::
+      { issubtype(X, union_type_1(arg_1)) }
+      issubtype(X, union_type_1(arg_1)) == (false || issubtype(X, arg_1)))
+  }
+
+  axiom union_subtype_2 {
+    (forall arg_1: PyType, arg_2: PyType, X: PyType ::
+      { issubtype(X, union_type_2(arg_1, arg_2)) }
+      issubtype(X, union_type_2(arg_1, arg_2)) ==
+      (false || issubtype(X, arg_1) || issubtype(X, arg_2)))
+  }
+
+  axiom union_subtype_3 {
+    (forall arg_1: PyType, arg_2: PyType, arg_3: PyType, X: PyType ::
+      { issubtype(X, union_type_3(arg_1, arg_2, arg_3)) }
+      issubtype(X, union_type_3(arg_1, arg_2, arg_3)) ==
+      (false || issubtype(X, arg_1) || issubtype(X, arg_2) ||
+      issubtype(X, arg_3)))
+  }
+
+  axiom union_subtype_4 {
+    (forall arg_1: PyType, arg_2: PyType, arg_3: PyType, arg_4: PyType, X: PyType ::
+      { issubtype(X, union_type_4(arg_1, arg_2, arg_3, arg_4)) }
+      issubtype(X, union_type_4(arg_1, arg_2, arg_3, arg_4)) ==
+      (false || issubtype(X, arg_1) || issubtype(X, arg_2) ||
+      issubtype(X, arg_3) ||
+      issubtype(X, arg_4)))
+  }
+
+  axiom subtype_union_1 {
+    (forall arg_1: PyType, X: PyType ::
+      { issubtype(union_type_1(arg_1), X) }
+      issubtype(union_type_1(arg_1), X) == (true && issubtype(arg_1, X)))
+  }
+
+  axiom subtype_union_2 {
+    (forall arg_1: PyType, arg_2: PyType, X: PyType ::
+      { issubtype(union_type_2(arg_1, arg_2), X) }
+      issubtype(union_type_2(arg_1, arg_2), X) ==
+      (true && issubtype(arg_1, X) && issubtype(arg_2, X)))
+  }
+
+  axiom subtype_union_3 {
+    (forall arg_1: PyType, arg_2: PyType, arg_3: PyType, X: PyType ::
+      { issubtype(union_type_3(arg_1, arg_2, arg_3), X) }
+      issubtype(union_type_3(arg_1, arg_2, arg_3), X) ==
+      (true && issubtype(arg_1, X) && issubtype(arg_2, X) &&
+      issubtype(arg_3, X)))
+  }
+
+  axiom subtype_union_4 {
+    (forall arg_1: PyType, arg_2: PyType, arg_3: PyType, arg_4: PyType, X: PyType ::
+      { issubtype(union_type_4(arg_1, arg_2, arg_3, arg_4), X) }
+      issubtype(union_type_4(arg_1, arg_2, arg_3, arg_4), X) ==
+      (true && issubtype(arg_1, X) && issubtype(arg_2, X) &&
+      issubtype(arg_3, X) &&
+      issubtype(arg_4, X)))
+  }
+
+  axiom subtype_list {
+    (forall var0: PyType ::
+      { list(var0) }
+      extends_(list(var0), object()) &&
+      get_basic(list(var0)) == list_basic())
+  }
+
+  axiom list_args0 {
+    (forall Z: PyType, arg0: PyType ::
+      { list(arg0), list_arg(Z, 0) }
+      issubtype(Z, list(arg0)) ==> list_arg(Z, 0) == arg0)
+  }
+
+  axiom subtype_set {
+    (forall var0: PyType ::
+      { set(var0) }
+      extends_(set(var0), object()) && get_basic(set(var0)) == set_basic())
+  }
+
+  axiom set_args0 {
+    (forall Z: PyType, arg0: PyType ::
+      { set(arg0), set_arg(Z, 0) }
+      issubtype(Z, set(arg0)) ==> set_arg(Z, 0) == arg0)
+  }
+
+  axiom subtype_dict {
+    (forall var0: PyType, var1: PyType ::
+      { dict(var0, var1) }
+      extends_(dict(var0, var1), object()) &&
+      get_basic(dict(var0, var1)) == dict_basic())
+  }
+
+  axiom dict_args0 {
+    (forall Z: PyType, arg0: PyType, arg1: PyType ::
+      { dict(arg0, arg1), dict_arg(Z, 0) }
+      issubtype(Z, dict(arg0, arg1)) ==> dict_arg(Z, 0) == arg0)
+  }
+
+  axiom dict_args1 {
+    (forall Z: PyType, arg0: PyType, arg1: PyType ::
+      { dict(arg0, arg1), dict_arg(Z, 1) }
+      issubtype(Z, dict(arg0, arg1)) ==> dict_arg(Z, 1) == arg1)
+  }
+
+  axiom subtype_int {
+    extends_(int(), float()) && get_basic(int()) == int()
+  }
+
+  axiom subtype_float {
+    extends_(float(), object()) && get_basic(float()) == float()
+  }
+
+  axiom subtype_bool {
+    extends_(bool(), int()) && get_basic(bool()) == bool()
+  }
+
+  axiom subtype_NoneType {
+    extends_(NoneType(), object()) && get_basic(NoneType()) == NoneType()
+  }
+
+  axiom subtype_Exception {
+    extends_(Exception(), object()) &&
+    get_basic(Exception()) == Exception()
+  }
+
+  axiom subtype_ConnectionRefusedError {
+    extends_(ConnectionRefusedError(), Exception()) &&
+    get_basic(ConnectionRefusedError()) == ConnectionRefusedError()
+  }
+
+  axiom subtype_traceback {
+    extends_(traceback(), object()) &&
+    get_basic(traceback()) == traceback()
+  }
+
+  axiom subtype_str {
+    extends_(str(), object()) && get_basic(str()) == str()
+  }
+
+  axiom subtype_bytes {
+    extends_(bytes(), object()) && get_basic(bytes()) == bytes()
+  }
+
+  axiom subtype_tuple {
+    (forall args: Seq[PyType] ::
+      { tuple(args) }
+      ((forall e: PyType ::(e in args) ==> e == object()) ==>
+      extends_(tuple(args), object())) &&
+      get_basic(tuple(args)) == tuple_basic())
+  }
+
+  axiom subtype_PSeq {
+    (forall var0: PyType ::
+      { PSeq(var0) }
+      extends_(PSeq(var0), object()) &&
+      get_basic(PSeq(var0)) == PSeq_basic())
+  }
+
+  axiom PSeq_args0 {
+    (forall Z: PyType, arg0: PyType ::
+      { PSeq(arg0), PSeq_arg(Z, 0) }
+      issubtype(Z, PSeq(arg0)) ==> PSeq_arg(Z, 0) == arg0)
+  }
+
+  axiom subtype_PSet {
+    (forall var0: PyType ::
+      { PSet(var0) }
+      extends_(PSet(var0), object()) &&
+      get_basic(PSet(var0)) == PSet_basic())
+  }
+
+  axiom PSet_args0 {
+    (forall Z: PyType, arg0: PyType ::
+      { PSet(arg0), PSet_arg(Z, 0) }
+      issubtype(Z, PSet(arg0)) ==> PSet_arg(Z, 0) == arg0)
+  }
+
+  axiom subtype_PMultiset {
+    (forall var0: PyType ::
+      { PMultiset(var0) }
+      extends_(PMultiset(var0), object()) &&
+      get_basic(PMultiset(var0)) == PMultiset_basic())
+  }
+
+  axiom PMultiset_args0 {
+    (forall Z: PyType, arg0: PyType ::
+      { PMultiset(arg0), PMultiset_arg(Z, 0) }
+      issubtype(Z, PMultiset(arg0)) ==> PMultiset_arg(Z, 0) == arg0)
+  }
+
+  axiom subtype_slice {
+    extends_(slice(), object()) && get_basic(slice()) == slice()
+  }
+
+  axiom subtype_range_0 {
+    extends_(range_0(), object()) && get_basic(range_0()) == range_0()
+  }
+
+  axiom subtype_Iterator {
+    (forall var0: PyType ::
+      { Iterator(var0) }
+      extends_(Iterator(var0), object()) &&
+      get_basic(Iterator(var0)) == Iterator_basic())
+  }
+
+  axiom Iterator_args0 {
+    (forall Z: PyType, arg0: PyType ::
+      { Iterator(arg0), Iterator_arg(Z, 0) }
+      issubtype(Z, Iterator(arg0)) ==> Iterator_arg(Z, 0) == arg0)
+  }
+
+  axiom subtype_Thread_0 {
+    extends_(Thread_0(), object()) && get_basic(Thread_0()) == Thread_0()
+  }
+
+  axiom subtype_LevelType {
+    extends_(LevelType(), object()) &&
+    get_basic(LevelType()) == LevelType()
+  }
+
+  axiom subtype_type {
+    extends_(type(), object()) && get_basic(type()) == type()
+  }
+
+  axiom subtype_Place {
+    extends_(Place(), object()) && get_basic(Place()) == Place()
+  }
+
+  axiom subtype___prim__Seq_type {
+    extends_(__prim__Seq_type(), object()) &&
+    get_basic(__prim__Seq_type()) == __prim__Seq_type()
+  }
+}
+
+domain SIFDomain[T]  {
+
+  function Low(x: T): Bool
+
+  axiom low_true {
+    (forall x: T :: { (Low(x): Bool) } (Low(x): Bool))
+  }
+}
+
+domain _list_ce_helper  {
+
+  function seq_ref_length(___s: Seq[Ref]): Int
+
+  function seq_ref_index(___s: Seq[Ref], i: Int): Ref
+
+  axiom relate_length {
+    (forall ___s: Seq[Ref] :: { |___s| } |___s| == seq_ref_length(___s))
+  }
+
+  axiom relate_index {
+    (forall ___s: Seq[Ref], ___i: Int ::
+      { ___s[___i] }
+      ___s[___i] == seq_ref_index(___s, ___i))
+  }
+}
+
+domain Measure$  {
+
+  function Measure$create(guard: Bool, key: Ref, value: Int): Measure$
+
+  function Measure$guard(m: Measure$): Bool
+
+  function Measure$key(m: Measure$): Ref
+
+  function Measure$value(m: Measure$): Int
+
+  axiom Measure$A0 {
+    (forall g: Bool, k: Ref, v: Int ::
+      { Measure$guard(Measure$create(g, k, v)) }
+      Measure$guard(Measure$create(g, k, v)) == g)
+  }
+
+  axiom Measure$A1 {
+    (forall g: Bool, k: Ref, v: Int ::
+      { Measure$key(Measure$create(g, k, v)) }
+      Measure$key(Measure$create(g, k, v)) == k)
+  }
+
+  axiom Measure$A2 {
+    (forall g: Bool, k: Ref, v: Int ::
+      { Measure$value(Measure$create(g, k, v)) }
+      Measure$value(Measure$create(g, k, v)) == v)
+  }
+}
+
+domain __MSHelper[T$]  {
+
+  function __toMS(s: Seq[T$]): Multiset[T$]
+
+  axiom __toMS_def_1 {
+    (__toMS(Seq[T$]()): Multiset[T$]) == Multiset[T$]()
+  }
+
+  axiom __toMS_def_2 {
+    (forall __t: T$ ::
+      { (__toMS(Seq(__t)): Multiset[T$]) }
+      (__toMS(Seq(__t)): Multiset[T$]) == Multiset(__t))
+  }
+
+  axiom __toMS_def_3 {
+    (forall __ss1: Seq[T$], __ss2: Seq[T$] ::
+      { (__toMS(__ss1 ++ __ss2): Multiset[T$]) }
+      (__toMS(__ss1 ++ __ss2): Multiset[T$]) ==
+      ((__toMS(__ss1): Multiset[T$]) union (__toMS(__ss2): Multiset[T$])))
+  }
+
+  axiom __toMS_def_4 {
+    (forall __ss1: Seq[T$] ::
+      { (__toMS(__ss1): Multiset[T$]) }
+      |(__toMS(__ss1): Multiset[T$])| == |__ss1|)
+  }
+}
+
+domain _Name  {
+
+  function _combine(n1: _Name, n2: _Name): _Name
+
+  function _single(n: Int): _Name
+
+  function _get_combined_prefix(n: _Name): _Name
+
+  function _get_combined_name(n: _Name): _Name
+
+  function _get_value(n: _Name): Int
+
+  function _name_type(n: _Name): Bool
+
+  function _is_single(n: _Name): Bool
+
+  function _is_combined(n: _Name): Bool
+
+  axiom decompose_single {
+    (forall i: Int :: { _single(i) } _get_value(_single(i)) == i)
+  }
+
+  axiom compose_single {
+    (forall n: _Name ::
+      { _get_value(n) }
+      _is_single(n) ==> n == _single(_get_value(n)))
+  }
+
+  axiom type_of_single {
+    (forall i: Int :: { _single(i) } _name_type(_single(i)))
+  }
+
+  axiom decompose_combined {
+    (forall n1: _Name, n2: _Name ::
+      { _combine(n1, n2) }
+      _get_combined_prefix(_combine(n1, n2)) == n1 &&
+      _get_combined_name(_combine(n1, n2)) == n2)
+  }
+
+  axiom compose_combined {
+    (forall n: _Name ::
+      { _get_combined_prefix(n) }
+      { _get_combined_name(n) }
+      _is_combined(n) ==>
+      n == _combine(_get_combined_prefix(n), _get_combined_name(n)))
+  }
+
+  axiom type_of_composed {
+    (forall n1: _Name, n2: _Name ::
+      { _combine(n1, n2) }
+      !_name_type(_combine(n1, n2)))
+  }
+
+  axiom type_is_single {
+    (forall n: _Name :: { _name_type(n) } _name_type(n) == _is_single(n))
+  }
+
+  axiom type_is_combined {
+    (forall n: _Name ::
+      { _name_type(n) }
+      !_name_type(n) == _is_combined(n))
+  }
+}
+
+domain IntWellFoundedOrder  {
+
+  axiom integer_ax_dec {
+    (forall int1: Int, int2: Int ::
+      { (decreasing(int1, int2): Bool) }
+      int1 < int2 ==> (decreasing(int1, int2): Bool))
+  }
+
+  axiom integer_ax_bound {
+    (forall int1: Int ::
+      { (bounded(int1): Bool) }
+      int1 >= 0 ==> (bounded(int1): Bool))
+  }
+}
+
+domain WellFoundedOrder[T]  {
+
+  function decreasing(arg1: T, arg2: T): Bool
+
+  function bounded(arg1: T): Bool
+}
+
+field _val: Ref
+
+field __container: Ref
+
+field __iter_index: Int
+
+field __previous: Seq[Ref]
+
+field list_acc: Seq[Ref]
+
+field set_acc: Set[Ref]
+
+field dict_acc: Map[Ref,Ref]
+
+field Measure$acc: Seq[Ref]
+
+field MustReleaseBounded: Int
+
+field MustReleaseUnbounded: Int
+
+function _isDefined(id: Int): Bool
+
+
+function __prim__int___box__(prim: Int): Ref
+  decreases _
+  ensures typeof(result) == int()
+  ensures int___unbox__(result) == prim
+
+
+function int___unbox__(box: Ref): Int
+  decreases _
+  requires issubtype(typeof(box), int())
+  ensures !issubtype(typeof(box), bool()) ==>
+    __prim__int___box__(result) == box
+  ensures issubtype(typeof(box), bool()) ==>
+    __prim__bool___box__(result != 0) == box
+
+
+function __prim__bool___box__(prim: Bool): Ref
+  decreases _
+  ensures typeof(result) == bool()
+  ensures bool___unbox__(result) == prim
+  ensures int___unbox__(result) == (prim ? 1 : 0)
+
+
+function bool___unbox__(box: Ref): Bool
+  decreases _
+  requires issubtype(typeof(box), bool())
+  ensures __prim__bool___box__(result) == box
+
+
+function int___gt__(self: Int, other: Int): Bool
+  decreases _
+{
+  self > other
+}
+
+function Level(r: Ref): Perm
+  decreases _
+
+
+predicate MustTerminate(r: Ref)
+
+predicate MustInvokeBounded(r: Ref)
+
+predicate MustInvokeUnbounded(r: Ref)
+
+predicate _MaySet(rec: Ref, id: Int)
+
+method main(_cthread_155: Ref, _caller_measures_155: Seq[Measure$], _residue_155: Perm,
+  x_0: Ref)
+  returns (_current_wait_level_155: Perm)
+  requires _cthread_155 != null
+  requires issubtype(typeof(_cthread_155), Thread_0())
+  requires issubtype(typeof(x_0), int())
+  requires int___gt__(int___unbox__(x_0), 10)
+  requires [true,
+    perm(MustTerminate(_cthread_155)) == none &&
+    ((forperm _r_1: Ref [MustInvokeBounded(_r_1)] :: false) &&
+    ((forperm _r_1: Ref [MustInvokeUnbounded(_r_1)] :: false) &&
+    ((forperm _r_1: Ref [_r_1.MustReleaseBounded] :: false) &&
+    (forperm _r_1: Ref [_r_1.MustReleaseUnbounded] :: false))))]
+{
+  var _err: Ref
+  var r: Ref
+  var x_1: Ref
+  var _cwl_155: Perm
+  var _method_measures_155: Seq[Measure$]
+  _method_measures_155 := Seq[Measure$]()
+  _err := null
+  x_1 := x_0
+  var huh: Int := 9
+  refute !int___gt__(int___unbox__(x_1), 0)
+  //:: ExpectedOutput(refute.failed:refutation.true)
+  refute int___gt__(int___unbox__(x_1), 0)  // should be an error
+  refute false
+  //:: ExpectedOutput(refute.failed:refutation.true)
+  refute true  // should be an error
+  refute false
+  if (int___gt__(int___unbox__(x_1), 0)) {
+    r := x_1
+    inhale _isDefined(114)
+  } else {
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    refute false  // should be an error
+    r := __prim__int___box__(0)
+    inhale _isDefined(114)
+  }
+  goto __end
+  label __end
+}
+

From c7d57c2e09eaec9279827098c93ec3a400e42702 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 21 Aug 2023 22:40:20 +0200
Subject: [PATCH 20/61] Adding test for Silicon issue 744

---
 src/test/resources/all/issues/silicon/0744.vpr | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0744.vpr

diff --git a/src/test/resources/all/issues/silicon/0744.vpr b/src/test/resources/all/issues/silicon/0744.vpr
new file mode 100644
index 000000000..045d864b0
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0744.vpr
@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+function fac(i: Int): Int
+  ensures ge(result, 1)
+{
+  i <= 1 ? 1 : i * fac(i - 1)
+}
+
+function ge(i1: Int, i2: Int): Bool
+{
+  i1 >= i2
+}
\ No newline at end of file

From 7681cd7f696182c206654eea01c90bfc9b9973ce Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 25 Aug 2023 16:17:54 +0200
Subject: [PATCH 21/61] Also checking postconditions for decreases for
 autoimport and predicate transformation

---
 .../plugin/standard/termination/TerminationPlugin.scala     | 6 +++---
 .../termination/functions/existingExamples/LinkedLists.sil  | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 85ed54c2d..d7b2754a9 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -104,10 +104,10 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
         decreasesClauses = decreasesClauses :+ dc
         dc
       case d => d
-    }).recurseFunc({ // decreases clauses can only appear in functions/methods pres and methods bodies
+    }).recurseFunc({ // decreases clauses can only appear in functions/methods pres, posts and methods bodies
       case PProgram(_, _, _, _, functions, _, methods, _, _) => Seq(functions, methods)
-      case PFunction(_, _, _, pres, _, _) => Seq(pres)
-      case PMethod(_, _, _, pres, _, body) => Seq(pres, body)
+      case PFunction(_, _, _, pres, posts, _) => Seq(pres, posts)
+      case PMethod(_, _, _, pres, posts, body) => Seq(pres, posts, body)
     }).execute(input)
 
     newProgram
diff --git a/src/test/resources/termination/functions/existingExamples/LinkedLists.sil b/src/test/resources/termination/functions/existingExamples/LinkedLists.sil
index 905741c51..091be4b69 100644
--- a/src/test/resources/termination/functions/existingExamples/LinkedLists.sil
+++ b/src/test/resources/termination/functions/existingExamples/LinkedLists.sil
@@ -11,9 +11,9 @@ predicate list(xs: Ref) {
 }
 
 function length(xs: Ref): Int
-  decreases list(xs)
   requires acc(list(xs)) && xs != null // (1)
   ensures result > 0
+  decreases list(xs)
 { unfolding acc(list(xs)) in 1 + (xs.next == null ? 0 : length(xs.next)) } // (1)
 
 function sum(xs: Ref): Int

From 6c83a1c3f129abf3115772071485821307f54347 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 6 Sep 2023 20:57:39 +0200
Subject: [PATCH 22/61] Generating decreasing and bounded axioms (used for
 termination checking) for declared ADTs (WIP)

---
 .../plugin/standard/adt/AdtPlugin.scala       |  4 +-
 .../standard/adt/encoding/AdtEncoder.scala    | 66 +++++++++++++++++--
 .../adt/encoding/AdtNameManager.scala         |  5 ++
 3 files changed, 70 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 982cecca5..511e39e89 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -34,6 +34,8 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     */
   private var derivesImported: Boolean = false
 
+  private def isTerminationPluginActive: Boolean = true // config != null && config.terminationPlugin.toOption.getOrElse(false)
+
   def adtDerivingFunc[$: P]: P[PIdnUse] = FP(StringIn("contains").!).map { case (pos, id) => PIdnUse(id)(pos) }
 
   override def beforeParse(input: String, isImported: Boolean): String = {
@@ -131,7 +133,7 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     if (deactivated) {
       return input
     }
-    new AdtEncoder(input).encode()
+    new AdtEncoder(input).encode(isTerminationPluginActive)
   }
 
 }
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
index 1392f79c3..3311d4f3b 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
@@ -32,13 +32,14 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     *
     * @return The encoded program.
     */
-  def encode(): Program = {
+  def encode(isTerminationPluginActive: Boolean): Program = {
 
     // In a first step encode all adt top level declarations and constructor calls
     var newProgram: Program = StrategyBuilder.Slim[Node]({
       case p@Program(domains, fields, functions, predicates, methods, extensions) =>
         val remainingExtensions = extensions filter { case _: Adt => false; case _ => true }
-        val encodedAdtsAsDomains: Seq[Domain] = extensions collect { case a: Adt => encodeAdtAsDomain(a) }
+        val tmp = extensions collect { case a: Adt => encodeAdtAsDomain(a, isTerminationPluginActive) }
+        val encodedAdtsAsDomains: Seq[Domain] = tmp.flatten
         Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT)
       case aca: AdtConstructorApp => encodeAdtConstructorApp(aca)
       case ada: AdtDestructorApp => encodeAdtDestructorApp(ada)
@@ -78,7 +79,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     * @param adt The ADT to encode
     * @return An the encoded ADT as a domain
     */
-  private def encodeAdtAsDomain(adt: Adt): Domain = {
+  private def encodeAdtAsDomain(adt: Adt, isTerminationPluginActive: Boolean): Seq[Domain] = {
     adt match {
       case Adt(name, constructors, typVars, derivingInfo) =>
         val domain = Domain(name, null, null, typVars)(adt.pos, adt.info, adt.errT)
@@ -88,7 +89,15 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
           (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors))
         val derivingAxioms = if (derivingInfo.contains(getContainsFunctionName))
           constructors filter (_.formalArgs.nonEmpty) map generateContainsAxiom(domain, derivingInfo(getContainsFunctionName)._2) else Seq.empty
-        domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT)
+        val newAdtDomain = domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT)
+
+        if (isTerminationPluginActive) {
+          val decreasesAxioms = constructors map generateDecreasesAxiom(domain)
+          val wellFoundedDomain = Domain(getWellFoundedDomainName(domain.name), Seq(), decreasesAxioms, domain.typVars)(adt.pos, adt.info, adt.errT)
+          Seq(newAdtDomain, wellFoundedDomain)
+        }else {
+          Seq(newAdtDomain)
+        }
     }
   }
 
@@ -427,6 +436,55 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT)
   }
 
+  private def generateDecreasesAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = {
+    assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")
+
+    val localVars = ac.formalArgs.map { lv =>
+      lv.typ match {
+        case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT)
+        case d => localVarTFromType(d, Some(lv.name))(ac.pos, ac.info, ac.errT)
+      }
+    }
+    val constructorApp = DomainFuncApp(
+      ac.name,
+      localVars,
+      defaultTypeVarsFromDomain(domain)
+    )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT)
+
+    val boundedApp = DomainFuncApp(
+      getBoundedFunctionName,
+      Seq(constructorApp),
+      Map(TypeVar("T") -> constructorApp.typ)
+    )(ac.pos, ac.info, Bool, getWellFoundedOrderDeclarationDomainName, ac.errT)
+
+
+    val body = if (ac.formalArgs.isEmpty) {
+      boundedApp
+    } else {
+      val localVarDecl = ac.formalArgs.collect { case l: LocalVarDecl => l }
+
+      assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.")
+
+      val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT)
+
+      val decreasesApp = (lv: LocalVar) => DomainFuncApp(
+        getDecreasesFunctionName,
+        Seq(lv, constructorApp),
+        Map(TypeVar("T") -> lv.typ)
+      )(ac.pos, ac.info, Bool, getWellFoundedOrderDeclarationDomainName, ac.errT)
+
+      val axiomBody = localVars.filter(lv => lv.typ == constructorApp.typ)
+        .map(decreasesApp)
+        .foldLeft[Exp](boundedApp)((a, b) => And(a, b)(ac.pos, ac.info, ac.errT)
+        )
+      val forall = Forall(localVarDecl, Seq(trigger), axiomBody)(ac.pos, ac.info, ac.errT)
+      forall
+    }
+
+
+    AnonymousDomainAxiom(body)(ac.pos, ac.info, ac.adtName, ac.errT)
+  }
+
   /**
     * This method encodes the transitivity of the contains function. Namely it collects arguments types of
     * all contains applications as tuples, computes its transitive closure and finally the corresponding axioms.
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala
index 812ac11eb..06628c801 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala
@@ -41,6 +41,11 @@ trait AdtNameManager {
 
   def getContainsFunctionName: String = "contains"
 
+  def getWellFoundedDomainName(typeName: String): String = typeName + "WellFoundedOrder"
+  def getWellFoundedOrderDeclarationDomainName : String = "WellFoundedOrder"
+  def getDecreasesFunctionName: String = "decreasing"
+  def getBoundedFunctionName: String = "bounded"
+
   def getContainsTransitivityDomain: String = getName("ContainsTransitivityDomain")
 
   /**

From 81e1b799e350c065a658d39da93b437099dd2394 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 3 Oct 2023 15:59:24 +0200
Subject: [PATCH 23/61] WIP

---
 .../viper/silver/frontend/SilFrontEndConfig.scala  |  4 ++--
 .../silver/plugin/standard/adt/AdtPlugin.scala     | 14 +++++++++++---
 .../plugin/standard/adt/encoding/AdtEncoder.scala  | 12 +++++++-----
 3 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
index cff594043..b837c5aed 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
@@ -110,7 +110,7 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     case i => throw new IllegalArgumentException(s"Unsupported counterexample model provided. Expected 'native', 'variables' or 'mapped' but got $i")
   }))
 
-  val terminationPlugin = opt[Boolean]("disableTerminationPlugin",
+  val disableTerminationPlugin = opt[Boolean]("disableTerminationPlugin",
     descr = "Disable the termination plugin, which adds termination checks to functions, " +
       "methods and loops.",
     default = Some(false),
@@ -118,7 +118,7 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = true
   )
 
-  val adtPlugin = opt[Boolean]("disableAdtPlugin",
+  val disableAdtPlugin = opt[Boolean]("disableAdtPlugin",
     descr = "Disable the ADT plugin, which adds support for ADTs as a built-in type.",
     default = Some(false),
     noshort = true,
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 511e39e89..7d4213f61 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -34,7 +34,15 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     */
   private var derivesImported: Boolean = false
 
-  private def isTerminationPluginActive: Boolean = true // config != null && config.terminationPlugin.toOption.getOrElse(false)
+  private def isTerminationPluginActive: Boolean = {
+    config != null && !config.disableTerminationPlugin.toOption.getOrElse(false) &&
+      (!config.disableDefaultPlugins.toOption.getOrElse(false) ||
+        config.plugin.toOption.getOrElse("").split(":").contains("viper.silver.plugin.standard.termination.TerminationPlugin"))
+  }
+
+  private def generateWellFoundednessAxioms(prog: Program): Boolean = {
+    isTerminationPluginActive && prog.domainsByName.contains("WellFoundedOrder")
+  }
 
   def adtDerivingFunc[$: P]: P[PIdnUse] = FP(StringIn("contains").!).map { case (pos, id) => PIdnUse(id)(pos) }
 
@@ -53,7 +61,7 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     input
   }
 
-  private def deactivated: Boolean = config != null && config.adtPlugin.toOption.getOrElse(false)
+  private def deactivated: Boolean = config != null && config.disableAdtPlugin.toOption.getOrElse(false)
 
   private def setDerivesImported(input: String): Unit = "import[\\s]+<adt\\/derives\\.vpr>".r.findFirstIn(input) match {
     case Some(_) => derivesImported = true
@@ -133,7 +141,7 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     if (deactivated) {
       return input
     }
-    new AdtEncoder(input).encode(isTerminationPluginActive)
+    new AdtEncoder(input).encode(generateWellFoundednessAxioms(input))
   }
 
 }
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
index 3311d4f3b..93fe03299 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
@@ -32,13 +32,13 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     *
     * @return The encoded program.
     */
-  def encode(isTerminationPluginActive: Boolean): Program = {
+  def encode(generateWellFoundedness: Boolean): Program = {
 
     // In a first step encode all adt top level declarations and constructor calls
     var newProgram: Program = StrategyBuilder.Slim[Node]({
       case p@Program(domains, fields, functions, predicates, methods, extensions) =>
         val remainingExtensions = extensions filter { case _: Adt => false; case _ => true }
-        val tmp = extensions collect { case a: Adt => encodeAdtAsDomain(a, isTerminationPluginActive) }
+        val tmp = extensions collect { case a: Adt => encodeAdtAsDomain(a, generateWellFoundedness) }
         val encodedAdtsAsDomains: Seq[Domain] = tmp.flatten
         Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT)
       case aca: AdtConstructorApp => encodeAdtConstructorApp(aca)
@@ -79,7 +79,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     * @param adt The ADT to encode
     * @return An the encoded ADT as a domain
     */
-  private def encodeAdtAsDomain(adt: Adt, isTerminationPluginActive: Boolean): Seq[Domain] = {
+  private def encodeAdtAsDomain(adt: Adt, generateWellFoundedness: Boolean): Seq[Domain] = {
     adt match {
       case Adt(name, constructors, typVars, derivingInfo) =>
         val domain = Domain(name, null, null, typVars)(adt.pos, adt.info, adt.errT)
@@ -91,7 +91,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
           constructors filter (_.formalArgs.nonEmpty) map generateContainsAxiom(domain, derivingInfo(getContainsFunctionName)._2) else Seq.empty
         val newAdtDomain = domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT)
 
-        if (isTerminationPluginActive) {
+        if (generateWellFoundedness) {
           val decreasesAxioms = constructors map generateDecreasesAxiom(domain)
           val wellFoundedDomain = Domain(getWellFoundedDomainName(domain.name), Seq(), decreasesAxioms, domain.typVars)(adt.pos, adt.info, adt.errT)
           Seq(newAdtDomain, wellFoundedDomain)
@@ -436,6 +436,8 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT)
   }
 
+  //private def generateDecreasesTransitivityAxiom(domain: Domain): AnonymousDomainAxiom = {}
+
   private def generateDecreasesAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = {
     assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")
 
@@ -470,7 +472,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
       val decreasesApp = (lv: LocalVar) => DomainFuncApp(
         getDecreasesFunctionName,
         Seq(lv, constructorApp),
-        Map(TypeVar("T") -> lv.typ)
+        Map(TypeVar("T") -> constructorApp.typ)
       )(ac.pos, ac.info, Bool, getWellFoundedOrderDeclarationDomainName, ac.errT)
 
       val axiomBody = localVars.filter(lv => lv.typ == constructorApp.typ)

From b22c402cbcb4e5552b0d2c455246069d02eec3b8 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 3 Oct 2023 16:52:33 +0200
Subject: [PATCH 24/61] Fixing Silicon issue #753

---
 .../silver/ast/utility/DomainInstances.scala  |  9 +-
 .../resources/all/issues/silicon/0751.vpr     | 12 +++
 .../resources/all/issues/silicon/0753.vpr     | 88 +++++++++++++++++++
 3 files changed, 106 insertions(+), 3 deletions(-)
 create mode 100644 src/test/resources/all/issues/silicon/0751.vpr
 create mode 100644 src/test/resources/all/issues/silicon/0753.vpr

diff --git a/src/main/scala/viper/silver/ast/utility/DomainInstances.scala b/src/main/scala/viper/silver/ast/utility/DomainInstances.scala
index c89803122..0883e1d2e 100644
--- a/src/main/scala/viper/silver/ast/utility/DomainInstances.scala
+++ b/src/main/scala/viper/silver/ast/utility/DomainInstances.scala
@@ -168,10 +168,13 @@ object DomainInstances {
           case Some(ps) =>
             ps.flatMap(f = pair => {
               //            assert(dfa.funcname==pair._1.funcname)
-              val d2 = p.findDomain(pair._2.domainName)
+              val d2 = p.findDomain(dfa.domainName)
               val tvs = d2.typVars
-              tryUnifyWithDefault(tvs, tvs.map(pair._1.typVarMap.getOrElse(_, Program.defaultType)), tvs.map(dfa.typVarMap.getOrElse(_, Program.defaultType))) match {
-                case Some(ts) => Set[Type](DomainType(pair._2.domainName, ts)(tvs))
+              val axDom = p.findDomain(pair._2.domainName)
+              val axTvs = axDom.typVars
+              tryUnifyWithDefault(axTvs, tvs.map(pair._1.typVarMap.get(_).get), tvs.map(dfa.typVarMap.get(_).get)) match {
+                case Some(ts) =>
+                  Set[Type](DomainType(pair._2.domainName, ts)(axTvs))
                 case None => Set[Type]()
               }
             }).toSet
diff --git a/src/test/resources/all/issues/silicon/0751.vpr b/src/test/resources/all/issues/silicon/0751.vpr
new file mode 100644
index 000000000..cfc92de6a
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0751.vpr
@@ -0,0 +1,12 @@
+domain $domain$to_int  {
+
+  function to_int(to_int1: Perm): Int interpretation "to_int"
+}
+
+function round(x: Perm): Perm
+  decreases
+  //:: ExpectedOutput(postcondition.violated:assertion.false)
+  ensures result == to_int(x) / 1
+{
+  to_int(x + (1/2)) / 1
+}
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silicon/0753.vpr b/src/test/resources/all/issues/silicon/0753.vpr
new file mode 100644
index 000000000..a7b1674ee
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0753.vpr
@@ -0,0 +1,88 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain Val  {}
+
+domain WellFoundedOrder[T]  {
+
+  function decreasing(arg1: T, arg2: T): Bool
+
+  function bounded(arg1: T): Bool
+}
+
+domain List[V]  {
+
+  function Nil(): List[V]
+
+  function Cons(value: V, tail: List[V]): List[V]
+
+  function get_List_value(t: List[V]): V
+
+  function get_List_tail(t: List[V]): List[V]
+
+  function List_tag(t: List[V]): Int
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      value == (get_List_value((Cons(value, tail): List[V])): V))
+  }
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      tail == (get_List_tail((Cons(value, tail): List[V])): List[V]))
+  }
+
+  axiom {
+    (List_tag((Nil(): List[V])): Int) == 1
+  }
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      (List_tag((Cons(value, tail): List[V])): Int) == 0)
+  }
+
+  axiom {
+    (forall t: List[V] ::
+      { (List_tag(t): Int) }
+      { (get_List_value(t): V) }
+      { (get_List_tail(t): List[V]) }
+      (List_tag(t) == 1 && t == (Nil(): List[V])) ||
+      (List_tag(t) == 0 && exists v: V, l: List[V] :: t == Cons(v, l))
+      //(t == (Cons((get_List_value(t): V), (get_List_tail(t): List[V])): List[V]))
+      )
+  }
+}
+
+domain ListWellFoundedOrder[V]  {
+
+  axiom {
+    (bounded((Nil(): List[V])): Bool)
+  }
+
+  axiom {
+    (forall value: V, tail: List[V] ::
+      { (Cons(value, tail): List[V]) }
+      (bounded((Cons(value, tail): List[V])): Bool) &&
+      (decreasing(tail, (Cons(value, tail): List[V])): Bool))
+  }
+}
+
+// decreases l
+function len(l: List[Val]): Int
+  ensures result >= 0
+{
+  ((List_tag(l): Int) == 1 ? 0 : 1 + len((get_List_tail(l): List[Val])))
+}
+
+// decreases l
+method len_termination_proof(l: List[Val])
+{
+  if ((List_tag(l): Int) == 1) {
+  } else {
+    assert (decreasing((get_List_tail(l): List[Val]), old(l)): Bool) &&
+      (bounded(old(l)): Bool)}
+}
\ No newline at end of file

From 47fbbd32fb22ff01c41851af7dca92489b88fe77 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 3 Oct 2023 16:58:24 +0200
Subject: [PATCH 25/61] Removing UnexpectedOutput annotation for fixed problem.

---
 src/test/resources/termination/functions/basic/allTypes.vpr | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/test/resources/termination/functions/basic/allTypes.vpr b/src/test/resources/termination/functions/basic/allTypes.vpr
index 04aa18733..4ada17c5e 100644
--- a/src/test/resources/termination/functions/basic/allTypes.vpr
+++ b/src/test/resources/termination/functions/basic/allTypes.vpr
@@ -85,7 +85,6 @@ function numberOfUsers(seq:Seq[Bool]): Int
 decreases seq
 {
     |seq| == 0 ? 0 :
-    //:: UnexpectedOutput(termination.failed:tuple.false, /silicon/issue/300/)
         seq[0] ? 1 + numberOfUsers(seq[1..]) : numberOfUsers(seq[1..])
 }
 

From 9d07532e953534f1410bb151c4307db7717cb0d1 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 3 Oct 2023 17:36:13 +0200
Subject: [PATCH 26/61] Things seem to work.

---
 .../viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala  | 2 +-
 .../silver/plugin/standard/termination/TerminationPlugin.scala  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
index 93fe03299..23f2f2093 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
@@ -484,7 +484,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     }
 
 
-    AnonymousDomainAxiom(body)(ac.pos, ac.info, ac.adtName, ac.errT)
+    AnonymousDomainAxiom(body)(ac.pos, ac.info, getWellFoundedDomainName(domain.name), ac.errT)
   }
 
   /**
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index d7b2754a9..2eed17348 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -29,7 +29,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
                         fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
   import fp.{FP, keyword, exp, ParserExtension}
 
-  private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)
+  private def deactivated: Boolean = config != null && config.disableTerminationPlugin.toOption.getOrElse(false)
 
   private var decreasesClauses: Seq[PDecreasesClause] = Seq.empty
 

From 0dccfad77dc5751ecc2d0ff8a98e75a2c87e1939 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 4 Oct 2023 15:05:05 +0200
Subject: [PATCH 27/61] Added transitivity axiom, added tests

---
 .../plugin/standard/adt/AdtPlugin.scala       |   6 +-
 .../standard/adt/encoding/AdtEncoder.scala    |  37 +++++-
 src/test/resources/adt/termination_1.vpr      | 105 ++++++++++++++++++
 src/test/resources/adt/termination_2.vpr      |  44 ++++++++
 src/test/resources/adt/termination_3.vpr      |  51 +++++++++
 .../resources/all/issues/silicon/0751.vpr     |   6 +-
 .../functions/basic/preventAutoImport.vpr     |  18 +++
 7 files changed, 257 insertions(+), 10 deletions(-)
 create mode 100644 src/test/resources/adt/termination_1.vpr
 create mode 100644 src/test/resources/adt/termination_2.vpr
 create mode 100644 src/test/resources/adt/termination_3.vpr
 create mode 100644 src/test/resources/termination/functions/basic/preventAutoImport.vpr

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 7d4213f61..d084ff995 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -40,10 +40,6 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
         config.plugin.toOption.getOrElse("").split(":").contains("viper.silver.plugin.standard.termination.TerminationPlugin"))
   }
 
-  private def generateWellFoundednessAxioms(prog: Program): Boolean = {
-    isTerminationPluginActive && prog.domainsByName.contains("WellFoundedOrder")
-  }
-
   def adtDerivingFunc[$: P]: P[PIdnUse] = FP(StringIn("contains").!).map { case (pos, id) => PIdnUse(id)(pos) }
 
   override def beforeParse(input: String, isImported: Boolean): String = {
@@ -141,7 +137,7 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     if (deactivated) {
       return input
     }
-    new AdtEncoder(input).encode(generateWellFoundednessAxioms(input))
+    new AdtEncoder(input).encode(isTerminationPluginActive)
   }
 
 }
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
index 23f2f2093..ca5b9b243 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
@@ -32,13 +32,18 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     *
     * @return The encoded program.
     */
-  def encode(generateWellFoundedness: Boolean): Program = {
+  def encode(isTerminationPluginActive: Boolean): Program = {
+    def generateWellFoundedness(a: Adt) =  {
+      isTerminationPluginActive &&
+        program.domainsByName.contains(getWellFoundedOrderDeclarationDomainName) &&
+        !program.domainsByName.contains(getWellFoundedDomainName(a.name))
+    }
 
     // In a first step encode all adt top level declarations and constructor calls
     var newProgram: Program = StrategyBuilder.Slim[Node]({
       case p@Program(domains, fields, functions, predicates, methods, extensions) =>
         val remainingExtensions = extensions filter { case _: Adt => false; case _ => true }
-        val tmp = extensions collect { case a: Adt => encodeAdtAsDomain(a, generateWellFoundedness) }
+        val tmp = extensions collect { case a: Adt => encodeAdtAsDomain(a, generateWellFoundedness(a)) }
         val encodedAdtsAsDomains: Seq[Domain] = tmp.flatten
         Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT)
       case aca: AdtConstructorApp => encodeAdtConstructorApp(aca)
@@ -92,7 +97,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
         val newAdtDomain = domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT)
 
         if (generateWellFoundedness) {
-          val decreasesAxioms = constructors map generateDecreasesAxiom(domain)
+          val decreasesAxioms = (constructors map generateDecreasesAxiom(domain)) :+ generateDecreasesTransitivityAxiom(domain)
           val wellFoundedDomain = Domain(getWellFoundedDomainName(domain.name), Seq(), decreasesAxioms, domain.typVars)(adt.pos, adt.info, adt.errT)
           Seq(newAdtDomain, wellFoundedDomain)
         }else {
@@ -436,7 +441,31 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT)
   }
 
-  //private def generateDecreasesTransitivityAxiom(domain: Domain): AnonymousDomainAxiom = {}
+  private def generateDecreasesTransitivityAxiom(domain: Domain): AnonymousDomainAxiom = {
+    val dt = DomainType(domain, defaultTypeVarsFromDomain(domain))
+    val v1 = LocalVarDecl("v1", dt)()
+    val v2 = LocalVarDecl("v2", dt)()
+    val v3 = LocalVarDecl("v3", dt)()
+    val decreases12 = DomainFuncApp(
+      getDecreasesFunctionName,
+      Seq(v1.localVar, v2.localVar),
+      Map(TypeVar("T") -> dt)
+    )(domain.pos, domain.info, Bool, getWellFoundedOrderDeclarationDomainName, domain.errT)
+    val decreases23 = DomainFuncApp(
+      getDecreasesFunctionName,
+      Seq(v2.localVar, v3.localVar),
+      Map(TypeVar("T") -> dt)
+    )(domain.pos, domain.info, Bool, getWellFoundedOrderDeclarationDomainName, domain.errT)
+    val decreases13 = DomainFuncApp(
+      getDecreasesFunctionName,
+      Seq(v1.localVar, v3.localVar),
+      Map(TypeVar("T") -> dt)
+    )(domain.pos, domain.info, Bool, getWellFoundedOrderDeclarationDomainName, domain.errT)
+    val trigger = Trigger(Seq(decreases12, decreases23))(domain.pos, domain.info, domain.errT)
+    val body = Implies(And(decreases12, decreases23)(domain.pos, domain.info, domain.errT), decreases13)(domain.pos, domain.info, domain.errT)
+    val forall = Forall(Seq(v1, v2, v3), Seq(trigger), body)()
+    AnonymousDomainAxiom(forall)(domain.pos, domain.info, getWellFoundedDomainName(domain.name), domain.errT)
+  }
 
   private def generateDecreasesAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = {
     assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")
diff --git a/src/test/resources/adt/termination_1.vpr b/src/test/resources/adt/termination_1.vpr
new file mode 100644
index 000000000..49ee5e507
--- /dev/null
+++ b/src/test/resources/adt/termination_1.vpr
@@ -0,0 +1,105 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain Val {}
+
+adt List[V] {
+    Nil()
+    Cons(value: V, tail: List[V])
+}
+
+function len(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : 1 + len(l.tail)
+}
+
+function len2(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : (l.tail.isNil ? 1 : 2 + len2(l.tail.tail))
+}
+
+function lenBad(l: List[Val], v: Val): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ lenBad(Cons(v, Nil()), v)
+}
+
+function lenBad2(l: List[Val]): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ 1 + lenBad2(l)
+}
+
+////////////////////////
+
+adt IntList {
+    INil()
+    ICons(ivalue: Int, itail: IntList)
+}
+
+function ilen(l: IntList): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isINil ? 0 : 1 + ilen(l.itail)
+}
+
+function ilen2(l: IntList): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isINil ? 0 : (l.itail.isINil ? 1 : 2 + ilen2(l.itail.itail))
+}
+
+function ilenBad(l: IntList, v: Int): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ ilenBad(ICons(v, INil()), v)
+}
+
+////////////////////////
+
+// non-recursive data type with two type variables
+adt Pair[T, V] {
+    pair(fst: T, snd: V)
+}
+
+function stupidFunc(p: Pair[Int, Val]): Val
+  decreases p
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  stupidFunc(p)
+}
+
+// two type variables
+adt DList[V, T] {
+    DNil()
+    DCons(dvalue1: V, dvalue2: T, dtail: DList[V, T])
+}
+
+function dlen(l: DList[Int, Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isDNil ? 0 : 1 + dlen(l.dtail)
+}
+
+function dlenBad(l: DList[Int, Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  l.isDNil ? 0 : 1 + dlenBad(l)
+}
+
diff --git a/src/test/resources/adt/termination_2.vpr b/src/test/resources/adt/termination_2.vpr
new file mode 100644
index 000000000..27f690422
--- /dev/null
+++ b/src/test/resources/adt/termination_2.vpr
@@ -0,0 +1,44 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+// Part of termination_1.vpr, but with the WellFoundedness domain already there.
+import <decreases/declaration.vpr>
+
+
+domain Val {}
+
+adt List[V] {
+    Nil()
+    Cons(value: V, tail: List[V])
+}
+
+function len(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : 1 + len(l.tail)
+}
+
+function len2(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  l.isNil ? 0 : (l.tail.isNil ? 1 : 2 + len2(l.tail.tail))
+}
+
+function lenBad(l: List[Val], v: Val): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ lenBad(Cons(v, Nil()), v)
+}
+
+function lenBad2(l: List[Val]): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ 1 + lenBad2(l)
+}
diff --git a/src/test/resources/adt/termination_3.vpr b/src/test/resources/adt/termination_3.vpr
new file mode 100644
index 000000000..a873c3ed2
--- /dev/null
+++ b/src/test/resources/adt/termination_3.vpr
@@ -0,0 +1,51 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+// Part of termination_1.vpr, but with the WellFoundedness domain already there and a custom domain for
+// the list well founded order.
+import <decreases/declaration.vpr>
+
+domain ListWellFoundedOrder[W] {
+    // Domain already being present will prevent auto-generation of axioms.
+    // Thus, we should not be able to prove termination based on List measures here.
+}
+
+domain Val {}
+
+adt List[V] {
+    Nil()
+    Cons(value: V, tail: List[V])
+}
+
+function len(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  l.isNil ? 0 : 1 + len(l.tail)
+}
+
+function len2(l: List[Val]): Int
+  ensures result >= 0
+  decreases l
+{
+  //:: ExpectedOutput(termination.failed:tuple.false)
+  l.isNil ? 0 : (l.tail.isNil ? 1 : 2 + len2(l.tail.tail))
+}
+
+function lenBad(l: List[Val], v: Val): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ lenBad(Cons(v, Nil()), v)
+}
+
+function lenBad2(l: List[Val]): Int
+ ensures result >= 0
+ decreases l
+{
+ //:: ExpectedOutput(termination.failed:tuple.false)
+ 1 + lenBad2(l)
+}
diff --git a/src/test/resources/all/issues/silicon/0751.vpr b/src/test/resources/all/issues/silicon/0751.vpr
index cfc92de6a..d57588aab 100644
--- a/src/test/resources/all/issues/silicon/0751.vpr
+++ b/src/test/resources/all/issues/silicon/0751.vpr
@@ -1,3 +1,6 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 domain $domain$to_int  {
 
   function to_int(to_int1: Perm): Int interpretation "to_int"
@@ -5,8 +8,9 @@ domain $domain$to_int  {
 
 function round(x: Perm): Perm
   decreases
+  ensures x == 3/1 ==> result == 3/2
   //:: ExpectedOutput(postcondition.violated:assertion.false)
   ensures result == to_int(x) / 1
 {
-  to_int(x + (1/2)) / 1
+  to_int(x) / 2
 }
\ No newline at end of file
diff --git a/src/test/resources/termination/functions/basic/preventAutoImport.vpr b/src/test/resources/termination/functions/basic/preventAutoImport.vpr
new file mode 100644
index 000000000..e5c3969e0
--- /dev/null
+++ b/src/test/resources/termination/functions/basic/preventAutoImport.vpr
@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+domain IntWellFoundedOrder{
+	// Domain already being present will prevent auto-import of the default domain.
+	// Thus, we have no defined order for type Int and proofs should fail.
+}
+
+//Example decreasing Int
+function fact(x:Int): Int
+  decreases x
+  requires x>=0
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    x==0 ? 1 : x*fact(x-1)
+}
\ No newline at end of file

From 34f63723b8cde58162d9cde39d0be3f734a4d98c Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 4 Oct 2023 15:07:38 +0200
Subject: [PATCH 28/61] Fixed test

---
 src/test/resources/all/issues/silicon/0751.vpr | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/test/resources/all/issues/silicon/0751.vpr b/src/test/resources/all/issues/silicon/0751.vpr
index cfc92de6a..c1441f41a 100644
--- a/src/test/resources/all/issues/silicon/0751.vpr
+++ b/src/test/resources/all/issues/silicon/0751.vpr
@@ -1,3 +1,7 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
 domain $domain$to_int  {
 
   function to_int(to_int1: Perm): Int interpretation "to_int"
@@ -5,8 +9,9 @@ domain $domain$to_int  {
 
 function round(x: Perm): Perm
   decreases
+  ensures x == 3/1 ==> result == 3/2
   //:: ExpectedOutput(postcondition.violated:assertion.false)
   ensures result == to_int(x) / 1
 {
-  to_int(x + (1/2)) / 1
+  to_int(x) / 2
 }
\ No newline at end of file

From e678cd731b4bc7dd7e9f79ae7627d08891158f2c Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 4 Oct 2023 23:42:17 +0200
Subject: [PATCH 29/61] New verification error for non-positive permissions,
 added test

---
 .../silver/verifier/VerificationError.scala   |  8 ++++
 src/test/resources/all/issues/silver/0444.vpr | 47 +++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 src/test/resources/all/issues/silver/0444.vpr

diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 67c0c66e0..208daaaa6 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -650,6 +650,14 @@ object reasons {
     def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = NegativePermission(offendingNode.asInstanceOf[Exp])
   }
 
+  case class NonPositivePermission(offendingNode: Exp) extends AbstractErrorReason {
+    val id = "permission.not.positive"
+
+    def readableMessage = s"Fraction $offendingNode might not be positive."
+
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = NonPositivePermission(offendingNode.asInstanceOf[Exp])
+  }
+
   case class InsufficientPermission(offendingNode: LocationAccess) extends AbstractErrorReason {
     val id = "insufficient.permission"
     def readableMessage = s"There might be insufficient permission to access $offendingNode"
diff --git a/src/test/resources/all/issues/silver/0444.vpr b/src/test/resources/all/issues/silver/0444.vpr
new file mode 100644
index 000000000..0e97c5a05
--- /dev/null
+++ b/src/test/resources/all/issues/silver/0444.vpr
@@ -0,0 +1,47 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+predicate falze()
+{
+    false
+}
+
+method test_unfold(){
+    //:: ExpectedOutput(unfold.failed:permission.not.positive)
+    unfold acc(falze(), none)
+    assert false
+}
+
+method test_unfold_unknown(p: Perm){
+    assume p >= none
+    //:: ExpectedOutput(unfold.failed:permission.not.positive)
+    unfold acc(falze(), p)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/34/)
+    assert false
+}
+
+method test_unfolding(){
+    //:: ExpectedOutput(assert.failed:permission.not.positive)
+    assert unfolding acc(falze(), none) in false
+}
+
+method test_unfolding_unknown(p: Perm){
+    assume p >= none
+    //:: ExpectedOutput(assert.failed:permission.not.positive)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/34/)
+    assert unfolding acc(falze(), p) in false
+}
+
+method test_fold(){
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
+    fold acc(falze(), none)
+}
+
+method test_fold_unknown(p: Perm){
+    assume p >= none
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
+    fold acc(falze(), p)
+}
\ No newline at end of file

From 67fa155884a51d17d25a496bda73d76b31a5c889 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 4 Oct 2023 23:57:49 +0200
Subject: [PATCH 30/61] Adapting tests

---
 src/test/resources/all/issues/carbon/0125.vpr | 10 +++++-----
 src/test/resources/all/issues/silver/0072.vpr | 10 +++++-----
 src/test/resources/all/issues/silver/0522.vpr |  2 +-
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/test/resources/all/issues/carbon/0125.vpr b/src/test/resources/all/issues/carbon/0125.vpr
index 4591edb71..38f38aca7 100644
--- a/src/test/resources/all/issues/carbon/0125.vpr
+++ b/src/test/resources/all/issues/carbon/0125.vpr
@@ -1,13 +1,13 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 predicate P(x: Ref) { acc(x.f) }
 
 method test1(x: Ref) {
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   unfold acc(P(x), -(1/2))
 }
 
@@ -16,7 +16,7 @@ method test2(x: Ref) {
   assume p == -(1/2)
 
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   unfold acc(P(x), p)
 }
 
diff --git a/src/test/resources/all/issues/silver/0072.vpr b/src/test/resources/all/issues/silver/0072.vpr
index 4b30f51a6..943d39dd6 100644
--- a/src/test/resources/all/issues/silver/0072.vpr
+++ b/src/test/resources/all/issues/silver/0072.vpr
@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 predicate token(x: Ref) {
@@ -16,14 +16,14 @@ method t_plus(x: Ref)
 method t_minus_1(x: Ref)
     requires acc(x.f)
 {
-    //:: ExpectedOutput(fold.failed:negative.permission)
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
     fold acc(token(x), (-1/1))
 }
 
 method t_minus_2(x: Ref)
     requires acc(x.f)
 {
-    //:: ExpectedOutput(fold.failed:negative.permission)
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
     fold acc(token(x), -(1/1))
 }
 
diff --git a/src/test/resources/all/issues/silver/0522.vpr b/src/test/resources/all/issues/silver/0522.vpr
index 69d694c71..107d47d11 100644
--- a/src/test/resources/all/issues/silver/0522.vpr
+++ b/src/test/resources/all/issues/silver/0522.vpr
@@ -27,7 +27,7 @@ method test3b(x: Ref, p: Perm) {
 
 method test4(x: Ref, p: Perm) {
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   //:: ExpectedOutput(unfold.failed:insufficient.permission)
   //:: MissingOutput(unfold.failed:insufficient.permission, /Silicon/issue/34/)
   unfold acc(P(x), p)

From 820db76e92646c57b180c7ccdc8dee0465118e62 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 5 Oct 2023 00:15:39 +0200
Subject: [PATCH 31/61] Fixed test for Carbon

---
 src/test/resources/all/issues/silver/0444.vpr | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/test/resources/all/issues/silver/0444.vpr b/src/test/resources/all/issues/silver/0444.vpr
index 0e97c5a05..9ab5c292b 100644
--- a/src/test/resources/all/issues/silver/0444.vpr
+++ b/src/test/resources/all/issues/silver/0444.vpr
@@ -7,6 +7,11 @@ predicate falze()
     false
 }
 
+predicate tru()
+{
+    true
+}
+
 method test_unfold(){
     //:: ExpectedOutput(unfold.failed:permission.not.positive)
     unfold acc(falze(), none)
@@ -16,9 +21,9 @@ method test_unfold(){
 method test_unfold_unknown(p: Perm){
     assume p >= none
     //:: ExpectedOutput(unfold.failed:permission.not.positive)
+    //:: ExpectedOutput(unfold.failed:insufficient.permission)
+    //:: MissingOutput(unfold.failed:insufficient.permission, /Silicon/issue/34/)
     unfold acc(falze(), p)
-    //:: ExpectedOutput(assert.failed:assertion.false)
-    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/34/)
     assert false
 }
 
@@ -30,18 +35,18 @@ method test_unfolding(){
 method test_unfolding_unknown(p: Perm){
     assume p >= none
     //:: ExpectedOutput(assert.failed:permission.not.positive)
-    //:: ExpectedOutput(assert.failed:assertion.false)
-    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/34/)
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    //:: MissingOutput(assert.failed:insufficient.permission, /Silicon/issue/34/)
     assert unfolding acc(falze(), p) in false
 }
 
 method test_fold(){
     //:: ExpectedOutput(fold.failed:permission.not.positive)
-    fold acc(falze(), none)
+    fold acc(tru(), none)
 }
 
 method test_fold_unknown(p: Perm){
     assume p >= none
     //:: ExpectedOutput(fold.failed:permission.not.positive)
-    fold acc(falze(), p)
+    fold acc(tru(), p)
 }
\ No newline at end of file

From 769b09f7071d2c97b50587dddbb7fce17fee1110 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 10 Oct 2023 15:13:45 +0200
Subject: [PATCH 32/61] Adding test for a Silicon wand issue

---
 .../resources/all/issues/silicon/0338.vpr     | 47 +++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0338.vpr

diff --git a/src/test/resources/all/issues/silicon/0338.vpr b/src/test/resources/all/issues/silicon/0338.vpr
new file mode 100644
index 000000000..4242d6b96
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0338.vpr
@@ -0,0 +1,47 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+function otherFunc(s: Seq[Int], i: Int): Bool
+    requires |s| > 1
+{
+  true
+}
+
+method foo(x: Ref, y: Ref, s: Seq[Int], i: Int)
+{
+    package (|s| > 3 ? (i > 1 && i < |s| - 2 && otherFunc(s, i)) : (i > 1 && i < |s| - 2))  --* true {
+    }
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert |s| > 0
+}
+
+
+field f: Int
+
+predicate p(x:Ref) {acc(x.f)}
+
+method tst(x: Ref)
+  requires acc(x.f, 1/2) && x.f == 3
+{
+    package acc(x.f, 1/2) && x.f == 2 --* p(x)
+    {
+        fold p(x)
+        assert x.f == 3
+    }
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+field data: Int
+
+method bar(x: Ref)
+    requires acc(x.data)
+{
+    package acc(x.data) --* false {
+        assert acc(x.data) && acc(x.data)
+        assert false
+    }
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
\ No newline at end of file

From 2258157ea591eae91d2f5596abb3ea8d5a3c87c6 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 10 Oct 2023 18:19:05 +0200
Subject: [PATCH 33/61] WIP

---
 .../standard/adt/encoding/AdtEncoder.scala    | 35 +++++++++++++++++++
 .../resources/adt/termination_mutual_1.vpr    |  0
 2 files changed, 35 insertions(+)
 create mode 100644 src/test/resources/adt/termination_mutual_1.vpr

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
index ca5b9b243..db37cc14c 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
@@ -504,6 +504,41 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
         Map(TypeVar("T") -> constructorApp.typ)
       )(ac.pos, ac.info, Bool, getWellFoundedOrderDeclarationDomainName, ac.errT)
 
+      def getNestedADTVals(visitedADTTypes: Set[AdtType], currentVar: LocalVarDecl): Seq[(Seq[LocalVarDecl], Exp, Exp)] = {
+        currentVar.typ match {
+          case at: AdtType if at == ac.typ => Seq((Seq(currentVar), currentVar.localVar, currentVar.localVar))
+          case at: AdtType if !visitedADTTypes.contains(at) =>
+            val adt = program.extensions.find {
+              case a: Adt if a.name == at.adtName => true
+              case _ => false
+            }.get.asInstanceOf[Adt]
+            // for every constructor,
+            // for every parameter, if there is something recursive to be done, collect options.
+            // if not, introduce a new quantified variable.
+            // if at least one parameter does something recursive, return the new plus returned quantified variables, the constructor
+            // applied to all args or lower level terms, and return the constrainable vars unchanged.
+            adt.constructors.flatMap(ac2 => {
+              val argDecls = ac2.formalArgs.map { case l: LocalVarDecl => l.copy(name = l.name + "_" + visitedADTTypes.size)(l.pos, l.info, l.errT) }
+              val argVals = ac2.formalArgs.map(fa2 => getNestedADTVals(visitedADTTypes + at, fa2))
+              argVals.zipWithIndex.flatMap{ case (avs, i) => {
+                val res: Seq[(Seq[LocalVarDecl], Exp, Exp)] = avs.map(av => {
+                  val qvars = av._1 ++ (argDecls diff Seq(argDecls(i)))
+                  val cApp = DomainFuncApp(
+                    ac2.name,
+                    argDecls.take(i).map(_.localVar) ++ Seq(av._2) ++ argDecls.drop(i + 1).map(_.localVar),
+                    encodeAdtTypeAsDomainType(ac2.typ).typVarsMap,
+                  )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac2.typ), ac.adtName, ac.errT)
+                  (qvars, cApp, av._3)
+                })
+                res
+              }}
+            })
+          case _ => Seq()
+        }
+      }
+
+      val nestedADTVals = localVarDecl.flatMap(lvd => getNestedADTVals(Set(), lvd))
+      println(nestedADTVals)
       val axiomBody = localVars.filter(lv => lv.typ == constructorApp.typ)
         .map(decreasesApp)
         .foldLeft[Exp](boundedApp)((a, b) => And(a, b)(ac.pos, ac.info, ac.errT)
diff --git a/src/test/resources/adt/termination_mutual_1.vpr b/src/test/resources/adt/termination_mutual_1.vpr
new file mode 100644
index 000000000..e69de29bb

From 76ea9b0ee419414af6d0db4d2204aab1ea78dcaa Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 11 Oct 2023 15:23:01 +0200
Subject: [PATCH 34/61] Supporting mutual recursion

---
 .../standard/adt/encoding/AdtEncoder.scala    | 77 +++++++++++--------
 .../resources/adt/termination_mutual_1.vpr    | 35 +++++++++
 2 files changed, 79 insertions(+), 33 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
index db37cc14c..6e7a05e36 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
@@ -97,7 +97,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
         val newAdtDomain = domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT)
 
         if (generateWellFoundedness) {
-          val decreasesAxioms = (constructors map generateDecreasesAxiom(domain)) :+ generateDecreasesTransitivityAxiom(domain)
+          val decreasesAxioms = (constructors map generateDecreasesAxiom(domain)) :+ generateDecreasesTransitivityAxiom(domain) :+ generateBoundedAxiom(domain)
           val wellFoundedDomain = Domain(getWellFoundedDomainName(domain.name), Seq(), decreasesAxioms, domain.typVars)(adt.pos, adt.info, adt.errT)
           Seq(newAdtDomain, wellFoundedDomain)
         }else {
@@ -467,6 +467,19 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(domain.pos, domain.info, getWellFoundedDomainName(domain.name), domain.errT)
   }
 
+  private def generateBoundedAxiom(domain: Domain): AnonymousDomainAxiom = {
+    val domainType = DomainType(domain, defaultTypeVarsFromDomain(domain))
+    val param = LocalVarDecl("x", domainType)()
+    val boundedApp = DomainFuncApp(
+      getBoundedFunctionName,
+      Seq(param.localVar),
+      Map(TypeVar("T") -> domainType)
+    )(domain.pos, domain.info, Bool, getWellFoundedOrderDeclarationDomainName, domain.errT)
+    val trigger = Trigger(Seq(boundedApp))(domain.pos, domain.info, domain.errT)
+    val forall = Forall(Seq(param), Seq(trigger), boundedApp)(domain.pos, domain.info, domain.errT)
+    AnonymousDomainAxiom(forall)(domain.pos, domain.info, getWellFoundedDomainName(domain.name), domain.errT)
+  }
+
   private def generateDecreasesAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = {
     assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")
 
@@ -476,33 +489,14 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
         case d => localVarTFromType(d, Some(lv.name))(ac.pos, ac.info, ac.errT)
       }
     }
-    val constructorApp = DomainFuncApp(
-      ac.name,
-      localVars,
-      defaultTypeVarsFromDomain(domain)
-    )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT)
 
-    val boundedApp = DomainFuncApp(
-      getBoundedFunctionName,
-      Seq(constructorApp),
-      Map(TypeVar("T") -> constructorApp.typ)
-    )(ac.pos, ac.info, Bool, getWellFoundedOrderDeclarationDomainName, ac.errT)
-
-
-    val body = if (ac.formalArgs.isEmpty) {
-      boundedApp
+    val decreases = if (ac.formalArgs.isEmpty) {
+      Nil
     } else {
       val localVarDecl = ac.formalArgs.collect { case l: LocalVarDecl => l }
 
       assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.")
 
-      val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT)
-
-      val decreasesApp = (lv: LocalVar) => DomainFuncApp(
-        getDecreasesFunctionName,
-        Seq(lv, constructorApp),
-        Map(TypeVar("T") -> constructorApp.typ)
-      )(ac.pos, ac.info, Bool, getWellFoundedOrderDeclarationDomainName, ac.errT)
 
       def getNestedADTVals(visitedADTTypes: Set[AdtType], currentVar: LocalVarDecl): Seq[(Seq[LocalVarDecl], Exp, Exp)] = {
         currentVar.typ match {
@@ -520,7 +514,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
             adt.constructors.flatMap(ac2 => {
               val argDecls = ac2.formalArgs.map { case l: LocalVarDecl => l.copy(name = l.name + "_" + visitedADTTypes.size)(l.pos, l.info, l.errT) }
               val argVals = ac2.formalArgs.map(fa2 => getNestedADTVals(visitedADTTypes + at, fa2))
-              argVals.zipWithIndex.flatMap{ case (avs, i) => {
+              argVals.zipWithIndex.flatMap{ case (avs, i) =>
                 val res: Seq[(Seq[LocalVarDecl], Exp, Exp)] = avs.map(av => {
                   val qvars = av._1 ++ (argDecls diff Seq(argDecls(i)))
                   val cApp = DomainFuncApp(
@@ -531,23 +525,40 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
                   (qvars, cApp, av._3)
                 })
                 res
-              }}
+              }
             })
           case _ => Seq()
         }
       }
+      var decreasesQuants: List[Exp] = Nil
+
+      val nestedADTVals = localVarDecl.map(lvd => getNestedADTVals(Set(), lvd))
+      for ((avs, i) <- nestedADTVals.zipWithIndex) {
+        val otherVars = localVarDecl.take(i) ++ localVarDecl.drop(i + 1)
+        for (av <- avs) {
+          val (qvars, value, smallerValue) = av
+          val allQvars = qvars ++ otherVars
+          val constructorArgs = localVars.take(i) ++ Seq(value) ++ localVars.drop(i + 1)
+          val constructorApp = DomainFuncApp(
+            ac.name,
+            constructorArgs,
+            defaultTypeVarsFromDomain(domain)
+          )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT)
+          val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT)
+          val decreasesApp = DomainFuncApp(
+            getDecreasesFunctionName,
+            Seq(smallerValue, constructorApp),
+            Map(TypeVar("T") -> constructorApp.typ)
+          )(ac.pos, ac.info, Bool, getWellFoundedOrderDeclarationDomainName, ac.errT)
+          val forall = Forall(allQvars, Seq(trigger), decreasesApp)(ac.pos, ac.info, ac.errT)
+          decreasesQuants = forall :: decreasesQuants
+        }
+      }
 
-      val nestedADTVals = localVarDecl.flatMap(lvd => getNestedADTVals(Set(), lvd))
-      println(nestedADTVals)
-      val axiomBody = localVars.filter(lv => lv.typ == constructorApp.typ)
-        .map(decreasesApp)
-        .foldLeft[Exp](boundedApp)((a, b) => And(a, b)(ac.pos, ac.info, ac.errT)
-        )
-      val forall = Forall(localVarDecl, Seq(trigger), axiomBody)(ac.pos, ac.info, ac.errT)
-      forall
+      decreasesQuants
     }
 
-
+    val body = decreases.foldLeft[Exp](TrueLit()())((a, b) => And(a, b)())
     AnonymousDomainAxiom(body)(ac.pos, ac.info, getWellFoundedDomainName(domain.name), ac.errT)
   }
 
diff --git a/src/test/resources/adt/termination_mutual_1.vpr b/src/test/resources/adt/termination_mutual_1.vpr
index e69de29bb..84205ba85 100644
--- a/src/test/resources/adt/termination_mutual_1.vpr
+++ b/src/test/resources/adt/termination_mutual_1.vpr
@@ -0,0 +1,35 @@
+adt List1 {
+  RList1(x: Int, l: List2)
+}
+adt List2 {
+  Empty()
+  NonEmpty(l: List1)
+}
+
+
+function len2(l: List2): Int
+    decreases l
+{
+    l == Empty()? 0 : 1 + len2(l.l.l)
+}
+
+
+function len2Bad(l: List2): Int
+    decreases l
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    l == Empty()? 0 : 1 + len2Bad(l)
+}
+
+function len1(l: List1): Int
+    decreases l
+{
+    l.l == Empty()? 0 : 1 + len1(l.l.l)
+}
+
+function len1Bad(l: List1): Int
+    decreases l
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    l.l == Empty()? 0 : 1 + len1Bad(l)
+}
\ No newline at end of file

From 4b08104f98d070bba668707b02e2f4de4c2ab279 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 11 Oct 2023 16:52:22 +0200
Subject: [PATCH 35/61] Documentation and better test for mutually recursive
 types

---
 .../standard/adt/encoding/AdtEncoder.scala    | 62 ++++++++++++---
 .../resources/adt/termination_mutual_1.vpr    | 75 ++++++++++++++++++-
 2 files changed, 127 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
index 6e7a05e36..96bb7d6c0 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala
@@ -441,6 +441,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT)
   }
 
+  /**
+    * Generates an axiom that expresses transitivity of the decreases relation for the current type ADT:
+    * forall v1: ADT, v2: ADT, v3: ADT :: { decreases(v1, v2), decreases(v2, v3) }
+    *   decreases(v1, v2) && decreases(v2, v3) ==> decreases(v1, v3)
+    */
   private def generateDecreasesTransitivityAxiom(domain: Domain): AnonymousDomainAxiom = {
     val dt = DomainType(domain, defaultTypeVarsFromDomain(domain))
     val v1 = LocalVarDecl("v1", dt)()
@@ -467,6 +472,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(domain.pos, domain.info, getWellFoundedDomainName(domain.name), domain.errT)
   }
 
+  /**
+    * Generates an axiom that expresses that all values of the current ADT are bounded:
+    * forall x: ADT :: { bounded(x) } bounded(x)
+    * This is justified by the fact that Viper ADTs are recursive types and are always finite.
+    */
   private def generateBoundedAxiom(domain: Domain): AnonymousDomainAxiom = {
     val domainType = DomainType(domain, defaultTypeVarsFromDomain(domain))
     val param = LocalVarDecl("x", domainType)()
@@ -480,6 +490,14 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     AnonymousDomainAxiom(forall)(domain.pos, domain.info, getWellFoundedDomainName(domain.name), domain.errT)
   }
 
+  /**
+    * Generates an axiom for the given constructor that expresses that all values of the current ADT contained
+    * inside an ADT value constructed using said constructor are smaller than the ADT value itself.
+    * E.g., for List { Nil() Cons(i: Int, l: List) }:
+    * forall i: Int, l: List :: { Cons(i, l) } decreases(l, Cons(i, l))
+    * Also takes into account values that may be contained through constructors of other ADT types (in cases of mutually
+    * recursive ADT definitions).
+    */
   private def generateDecreasesAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = {
     assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")
 
@@ -497,25 +515,47 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
 
       assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.")
 
-
+      /**
+        * Given a variable currentVar that represents an argument of the current ADT constructor, if the variable's
+        * type is an ADT type, recursively looks for values of the original ADT type, either in the variable itself
+        * or in all constructors of its type.
+        * E.g., if ac is a constructor for ADT1, then:
+        *  - if the type of currentVar is ADT1, then we have already found a value of the original ADT type
+        *  - if the type of the variable is ADT2, and ADT2 has a constructor C(T1, ADT1), then we have found a value
+        *    of the original type inside this constructor.
+        * The method returns a sequence of tuples, where each tuple contains
+        * - a list of all variables referred to in the second argument
+        * - an expression containing a value of type ADT1 (either just a variable of the type, or an ADT constructor
+        *   applied to some arguments, one of which is either itself a variable of type ADT1 or another ADT constructor
+        *   that has an argument that is or contains a value of said type).
+        * - the variable of type ADT1 contained in the second term.
+        * So, in the first scenario above, we return Seq((Seq(currentVar), currentVar, currentVar)).
+        * In the second scenario, we return Seq((Seq(t: T, a: ADT1), C(t, a), a))
+        */
       def getNestedADTVals(visitedADTTypes: Set[AdtType], currentVar: LocalVarDecl): Seq[(Seq[LocalVarDecl], Exp, Exp)] = {
         currentVar.typ match {
-          case at: AdtType if at == ac.typ => Seq((Seq(currentVar), currentVar.localVar, currentVar.localVar))
+          case at: AdtType if at == ac.typ =>
+            // case 1: The variable directly has the type that we are looking for.
+            val newName = currentVar.name + "_" + visitedADTTypes.size
+            val renamedCurrentVar = currentVar.copy(name = newName)(currentVar.pos, currentVar.info, currentVar.errT)
+            Seq((Seq(renamedCurrentVar), renamedCurrentVar.localVar, renamedCurrentVar.localVar))
           case at: AdtType if !visitedADTTypes.contains(at) =>
+            // case 2: The variable has a different ADT type, which may have one or more constructors that contain
+            // a value of the type we are looking for.
             val adt = program.extensions.find {
               case a: Adt if a.name == at.adtName => true
               case _ => false
             }.get.asInstanceOf[Adt]
-            // for every constructor,
-            // for every parameter, if there is something recursive to be done, collect options.
-            // if not, introduce a new quantified variable.
-            // if at least one parameter does something recursive, return the new plus returned quantified variables, the constructor
-            // applied to all args or lower level terms, and return the constrainable vars unchanged.
+
+            // Look through all constructors
             adt.constructors.flatMap(ac2 => {
               val argDecls = ac2.formalArgs.map { case l: LocalVarDecl => l.copy(name = l.name + "_" + visitedADTTypes.size)(l.pos, l.info, l.errT) }
+
+              // Recursively check the type of the constructor's arguments
               val argVals = ac2.formalArgs.map(fa2 => getNestedADTVals(visitedADTTypes + at, fa2))
               argVals.zipWithIndex.flatMap{ case (avs, i) =>
                 val res: Seq[(Seq[LocalVarDecl], Exp, Exp)] = avs.map(av => {
+                  // Apply the current constructor to the arguments for every occurrence that was found.
                   val qvars = av._1 ++ (argDecls diff Seq(argDecls(i)))
                   val cApp = DomainFuncApp(
                     ac2.name,
@@ -527,12 +567,17 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
                 res
               }
             })
-          case _ => Seq()
+          case _ =>
+            // case 3: Different type or an ADT type we already looked at.
+            Seq()
         }
       }
       var decreasesQuants: List[Exp] = Nil
 
       val nestedADTVals = localVarDecl.map(lvd => getNestedADTVals(Set(), lvd))
+
+      // For each found nested value of our type, generate a quantified expression that states states that the contained
+      // value is less than the original value.
       for ((avs, i) <- nestedADTVals.zipWithIndex) {
         val otherVars = localVarDecl.take(i) ++ localVarDecl.drop(i + 1)
         for (av <- avs) {
@@ -554,7 +599,6 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
           decreasesQuants = forall :: decreasesQuants
         }
       }
-
       decreasesQuants
     }
 
diff --git a/src/test/resources/adt/termination_mutual_1.vpr b/src/test/resources/adt/termination_mutual_1.vpr
index 84205ba85..286a4f3eb 100644
--- a/src/test/resources/adt/termination_mutual_1.vpr
+++ b/src/test/resources/adt/termination_mutual_1.vpr
@@ -1,9 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// Mutually recursive ADTs
 adt List1 {
   RList1(x: Int, l: List2)
 }
 adt List2 {
   Empty()
-  NonEmpty(l: List1)
+  NonEmpty(x: Int, l: List1)
 }
 
 
@@ -32,4 +36,73 @@ function len1Bad(l: List1): Int
 {
     //:: ExpectedOutput(termination.failed:tuple.false)
     l.l == Empty()? 0 : 1 + len1Bad(l)
+}
+
+// Name clash between y: MList2 and y: Int
+adt MList1 {
+  MRList1(x: Int, y: MList2)
+}
+adt MList2 {
+  MEmpty()
+  MNonEmpty(y: Int, l: MList1)
+}
+
+
+function mlen2(l: MList2): Int
+    decreases l
+{
+    l == MEmpty()? 0 : 1 + mlen2(l.l.y)
+}
+
+// Three mutually recursive types
+adt Triple1 {
+  triple1(x: Triple2)
+}
+
+adt Triple2 {
+  triple2(x: Triple3)
+}
+
+adt Triple3 {
+  triple3(x: Triple1)
+  nil(i: Int)
+}
+
+function tripleLen1(t: Triple1): Int
+    decreases t
+{
+    2 + (t.x.x.isnil ? 0 : tripleLen1(t.x.x.x))
+}
+
+function tripleLen2(t: Triple2): Int
+    decreases t
+{
+    1 + (t.x.isnil ? 0 : (1 + tripleLen2(t.x.x.x)))
+}
+
+function tripleLen3(t: Triple3): Int
+    decreases t
+{
+    t.isnil ? 0 : (3 + tripleLen3(t.x.x.x))
+}
+
+function tripleLen1Bad(t: Triple1): Int
+    decreases t
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    2 + (t.x.x.isnil ? 0 : tripleLen1Bad(t))
+}
+
+function tripleLen2Bad(t: Triple2): Int
+    decreases t
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    1 + (t.x.isnil ? 0 : (1 + tripleLen2Bad(t)))
+}
+
+function tripleLen3Bad(t: Triple3): Int
+    decreases t
+{
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    t.isnil ? 0 : (3 + tripleLen3Bad(t))
 }
\ No newline at end of file

From 7edf26b773802ffc6c990ffd0ef9b6acd8065fd1 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 16 Oct 2023 17:02:10 +0200
Subject: [PATCH 36/61] Added test annotation for Carbon

---
 src/test/resources/all/issues/silicon/0338.vpr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/test/resources/all/issues/silicon/0338.vpr b/src/test/resources/all/issues/silicon/0338.vpr
index 4242d6b96..7da5843bd 100644
--- a/src/test/resources/all/issues/silicon/0338.vpr
+++ b/src/test/resources/all/issues/silicon/0338.vpr
@@ -40,6 +40,7 @@ method bar(x: Ref)
 {
     package acc(x.data) --* false {
         assert acc(x.data) && acc(x.data)
+        //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/470/)
         assert false
     }
     //:: ExpectedOutput(assert.failed:assertion.false)

From a48b4a0c62c1728791ab41e3554767b8d5b716a4 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 18 Oct 2023 17:49:01 +0200
Subject: [PATCH 37/61] Cleaner implementation of fix for issue #740

---
 .../ast/utility/GenericTriggerGenerator.scala       | 10 ++++++++++
 .../scala/viper/silver/ast/utility/Triggers.scala   | 13 +++++++++++++
 2 files changed, 23 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
index e6e37edda..b890b48df 100644
--- a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
+++ b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
@@ -8,6 +8,7 @@ package viper.silver.ast.utility
 
 import java.util.concurrent.atomic.AtomicInteger
 import reflect.ClassTag
+import viper.silver.ast
 
 object GenericTriggerGenerator {
   case class TriggerSet[E](exps: Seq[E])
@@ -195,10 +196,19 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
         else
           results.flatten
 
+      case e if modifyPossibleTriggers.isDefinedAt(e) => modifyPossibleTriggers.apply(e)(results)
+
       case _ => results.flatten
     })
   }
 
+  /*
+   * Hook for clients to add more cases to getFunctionAppsContaining to modify the found possible triggers.
+   * Used e.g. to wrap trigger expressions inferred from inside old-expression into old()
+   */
+  def modifyPossibleTriggers: PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] =>
+    Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] = PartialFunction.empty
+
   /* Precondition: if vars is non-empty then every (f,vs) pair in functs
    * satisfies the property that vars and vs are not disjoint.
    *
diff --git a/src/main/scala/viper/silver/ast/utility/Triggers.scala b/src/main/scala/viper/silver/ast/utility/Triggers.scala
index f561512ef..93b89e609 100644
--- a/src/main/scala/viper/silver/ast/utility/Triggers.scala
+++ b/src/main/scala/viper/silver/ast/utility/Triggers.scala
@@ -57,6 +57,19 @@ object Triggers {
       case LabelledOld(pt: PossibleTrigger, _) => pt.getArgs
       case _ => sys.error(s"Unexpected expression $e")
     }
+
+    override def modifyPossibleTriggers = {
+      case ast.Old(_) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          (ast.Old(exp)(exp.pos, exp.info, exp.errT), t._2, t._3)
+        })
+      case ast.LabelledOld(_, l) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          (ast.LabelledOld(exp, l)(exp.pos, exp.info, exp.errT), t._2, t._3)
+        })
+    }
   }
 
   /**

From 25be372034c46a8236af0c02f74fb3a1571b9539 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 18 Oct 2023 17:51:55 +0200
Subject: [PATCH 38/61] Removed unnecessary import

---
 .../scala/viper/silver/ast/utility/GenericTriggerGenerator.scala | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
index b890b48df..35f98c242 100644
--- a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
+++ b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
@@ -8,7 +8,6 @@ package viper.silver.ast.utility
 
 import java.util.concurrent.atomic.AtomicInteger
 import reflect.ClassTag
-import viper.silver.ast
 
 object GenericTriggerGenerator {
   case class TriggerSet[E](exps: Seq[E])

From 7b1c871bf3e0c83f4036614b8f9982b40515c54b Mon Sep 17 00:00:00 2001
From: Pieter Bos <p.h.bos@utwente.nl>
Date: Mon, 23 Oct 2023 10:56:30 +0200
Subject: [PATCH 39/61] seal VerificationError and ErrorReason

---
 .../PredicateInstanceErrors.scala                  |  6 ++++--
 .../plugin/standard/refute/RefuteErrors.scala      |  7 +++++--
 .../standard/termination/TerminationErrors.scala   | 14 ++++++++------
 .../viper/silver/verifier/VerificationError.scala  | 12 ++++++++----
 src/test/scala/IOTests.scala                       |  4 +++-
 5 files changed, 28 insertions(+), 15 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstanceErrors.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstanceErrors.scala
index fb6c139e6..2d7d44ceb 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstanceErrors.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstanceErrors.scala
@@ -6,10 +6,12 @@
 
 package viper.silver.plugin.standard.predicateinstance
 
-import viper.silver.verifier.{AbstractVerificationError, ErrorMessage, ErrorReason}
+import viper.silver.verifier.{AbstractVerificationError, ErrorMessage, ErrorReason, ExtensionAbstractVerificationError}
 import viper.silver.verifier.reasons.ErrorNode
 
-case class PredicateInstanceNoAccess(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean) extends AbstractVerificationError {
+sealed abstract class PredicateInstanceError extends ExtensionAbstractVerificationError
+
+case class PredicateInstanceNoAccess(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean) extends PredicateInstanceError {
   override protected def text: String = "Accessing predicate instance might fail."
 
   override def withReason(reason: ErrorReason): AbstractVerificationError = PredicateInstanceNoAccess(this.offendingNode, this.reason, cached)
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
index b75560bab..e3642b52a 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
@@ -8,7 +8,10 @@ package viper.silver.plugin.standard.refute
 
 import viper.silver.verifier._
 
-case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
+sealed abstract class RefuteError extends ExtensionAbstractVerificationError
+sealed abstract class RefuteErrorReason extends ExtensionAbstractErrorReason
+
+case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends RefuteError {
   override val id = "refute.failed"
   override val text = "Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)."
 
@@ -18,7 +21,7 @@ case class RefuteFailed(override val offendingNode: Refute, override val reason:
   override def withReason(r: ErrorReason): RefuteFailed = RefuteFailed(offendingNode, r, cached)
 }
 
-case class RefutationTrue(offendingNode: reasons.ErrorNode) extends AbstractErrorReason {
+case class RefutationTrue(offendingNode: reasons.ErrorNode) extends RefuteErrorReason {
   override val id: String = "refutation.true"
 
   override val readableMessage: String = s"Assertion $offendingNode definitely holds."
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationErrors.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationErrors.scala
index b667d5b6b..f6bcaf178 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationErrors.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationErrors.scala
@@ -17,10 +17,12 @@ import viper.silver.verifier._
 /**
  * Error for all termination related failed assertions.
  */
-abstract class AbstractTerminationError() extends AbstractVerificationError {
+sealed abstract class AbstractTerminationError extends ExtensionAbstractVerificationError {
   override val id = "termination.failed"
 }
 
+sealed abstract class TerminationErrorReason extends ExtensionAbstractErrorReason
+
 case class FunctionTerminationError(override val offendingNode: ErrorNode,
                                     override val reason: ErrorReason,
                                     override val cached: Boolean = false) extends AbstractTerminationError {
@@ -59,7 +61,7 @@ case class LoopTerminationError(override val offendingNode: ErrorNode,
  Reasons for all termination related failed assertions.
  */
 
-case class TerminationConditionFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TerminationConditionFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "termination.condition.false"
 
   override val readableMessage: String = s"Required termination condition might not hold."
@@ -67,7 +69,7 @@ case class TerminationConditionFalse(offendingNode: ErrorNode) extends AbstractE
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TerminationConditionFalse(offendingNode)
 }
 
-case class TupleConditionFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleConditionFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.condition.false"
 
   override val readableMessage: String = s"Required tuple condition might not hold."
@@ -75,7 +77,7 @@ case class TupleConditionFalse(offendingNode: ErrorNode) extends AbstractErrorRe
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TupleConditionFalse(offendingNode)
 }
 
-case class TupleSimpleFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleSimpleFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.false"
 
   override val readableMessage: String = s"Termination measure might not decrease or might not be bounded."
@@ -83,7 +85,7 @@ case class TupleSimpleFalse(offendingNode: ErrorNode) extends AbstractErrorReaso
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TupleSimpleFalse(offendingNode)
 }
 
-case class TupleDecreasesFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleDecreasesFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.false"
 
   override val readableMessage: String = s"Termination measure might not decrease."
@@ -91,7 +93,7 @@ case class TupleDecreasesFalse(offendingNode: ErrorNode) extends AbstractErrorRe
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TupleDecreasesFalse(offendingNode)
 }
 
-case class TupleBoundedFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleBoundedFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.false"
 
   override val readableMessage: String = s"Termination measure might not bounded."
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 208daaaa6..4ee3f6d45 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -160,7 +160,7 @@ trait ErrorMessage {
   }
 }
 
-trait VerificationError extends AbstractError with ErrorMessage {
+sealed trait VerificationError extends AbstractError with ErrorMessage {
   def reason: ErrorReason
   def readableMessage(withId: Boolean = false, withPosition: Boolean = false): String
   override def readableMessage: String = {
@@ -196,7 +196,7 @@ case object DummyReason extends AbstractErrorReason {
   def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = DummyReason
 }
 
-trait ErrorReason extends ErrorMessage
+sealed trait ErrorReason extends ErrorMessage
 
 trait PartialVerificationError {
   def f: ErrorReason => VerificationError
@@ -226,7 +226,7 @@ case object NullPartialVerificationError extends PartialVerificationError {
   def f = _ => null
 }
 
-abstract class AbstractVerificationError extends VerificationError {
+sealed abstract class AbstractVerificationError extends VerificationError {
   protected def text: String
 
   def pos = offendingNode.pos
@@ -253,11 +253,15 @@ abstract class AbstractVerificationError extends VerificationError {
   override def toString = readableMessage(true, true) + (if (cached) " - cached" else "")
 }
 
-abstract class AbstractErrorReason extends ErrorReason {
+abstract class ExtensionAbstractVerificationError extends AbstractVerificationError
+
+sealed abstract class AbstractErrorReason extends ErrorReason {
   def pos = offendingNode.pos
   override def toString = readableMessage
 }
 
+abstract class ExtensionAbstractErrorReason extends AbstractErrorReason
+
 object errors {
   type ErrorNode = Node with Positioned with TransformableErrors with Rewritable
 
diff --git a/src/test/scala/IOTests.scala b/src/test/scala/IOTests.scala
index 9ef10b6e4..e0ca146ba 100644
--- a/src/test/scala/IOTests.scala
+++ b/src/test/scala/IOTests.scala
@@ -165,7 +165,7 @@ class IOTests extends AnyFunSuite with Matchers {
 
     override def verify(program: Program): VerificationResult = {
       if (pass) Success
-      else Failure(Seq(new VerificationError {
+      else Failure(Seq(new ExtensionAbstractVerificationError {
         override def reason: ErrorReason = DummyReason
         override def readableMessage(withId: Boolean, withPosition: Boolean): String =
           "MockIOVerifier failed the verification (as requested)."
@@ -173,6 +173,8 @@ class IOTests extends AnyFunSuite with Matchers {
         override def pos: Position = NoPosition
         override def offendingNode: ErrorNode = DummyNode
         override def id: String = "MockIOVerifier.verification.failure"
+        override protected def text: String = ""
+        override def withReason(reason: ErrorReason): AbstractVerificationError = this
       }))
     }
 

From 69b4a8e158c4da9679f93fc24bb91a0e1517ecf9 Mon Sep 17 00:00:00 2001
From: Pieter Bos <p.h.bos@utwente.nl>
Date: Mon, 23 Oct 2023 11:08:11 +0200
Subject: [PATCH 40/61] test: fix mock withNode

---
 src/test/scala/IOTests.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/scala/IOTests.scala b/src/test/scala/IOTests.scala
index e0ca146ba..5b4b38412 100644
--- a/src/test/scala/IOTests.scala
+++ b/src/test/scala/IOTests.scala
@@ -169,7 +169,7 @@ class IOTests extends AnyFunSuite with Matchers {
         override def reason: ErrorReason = DummyReason
         override def readableMessage(withId: Boolean, withPosition: Boolean): String =
           "MockIOVerifier failed the verification (as requested)."
-        override def withNode(offendingNode: ErrorNode): ErrorMessage = DummyReason
+        override def withNode(offendingNode: ErrorNode): ErrorMessage = this
         override def pos: Position = NoPosition
         override def offendingNode: ErrorNode = DummyNode
         override def id: String = "MockIOVerifier.verification.failure"

From d43db152cf930e4e1c6b79fd1fc67837c93829b7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 31 Oct 2023 13:27:58 +0100
Subject: [PATCH 41/61] Test for @opaque() function annotation

---
 src/test/resources/all/functions/opaque.vpr | 296 ++++++++++++++++++++
 1 file changed, 296 insertions(+)
 create mode 100644 src/test/resources/all/functions/opaque.vpr

diff --git a/src/test/resources/all/functions/opaque.vpr b/src/test/resources/all/functions/opaque.vpr
new file mode 100644
index 000000000..401c9506b
--- /dev/null
+++ b/src/test/resources/all/functions/opaque.vpr
@@ -0,0 +1,296 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+// use function and dont know def
+// recursive
+
+@opaque()
+function isGreaterOne(i: Int): Bool
+    requires i > -60
+    ensures (i > 60) ==> result
+{ i > 1 }
+
+@opaque()
+function isGreaterOne2(r: Ref): Bool
+    requires acc(r.f) && r.f > -38
+    ensures (r.f > 60) ==> result
+{ isGreaterOne(r.f) }
+
+@opaque()
+function isGreaterOne22(r: Ref): Bool
+    requires acc(r.f) && r.f > -38
+    ensures (r.f > 60) ==> result
+    //:: ExpectedOutput(postcondition.violated:assertion.false)
+    ensures result == r.f > 1 // fail
+{ isGreaterOne(r.f) }
+
+@opaque()
+function isGreaterOne3(r: Ref): Bool
+    requires acc(r.f) && r.f > -38
+    ensures (r.f > 60) ==> result
+{ @reveal() isGreaterOne(r.f) }
+
+@opaque()
+function isGreaterOne32(r: Ref): Bool
+    requires acc(r.f) && r.f > -38
+    ensures (r.f > 60) ==> result
+    ensures result == r.f > 1
+{ @reveal() isGreaterOne(r.f) }
+
+@opaque()
+function isGreaterOne33(r: Ref): Bool
+    requires acc(r.f)
+    ensures (r.f > 60) ==> result
+    ensures result == r.f > 1
+//:: ExpectedOutput(application.precondition:assertion.false)
+{ @reveal() isGreaterOne(r.f) }
+
+function isGreaterOne34(r: Ref): Bool
+    requires acc(r.f) && r.f > -38
+    ensures (r.f > 60) ==> result
+{ @reveal() isGreaterOne(r.f) }
+
+function isGreaterOne35(r: Ref): Bool
+    requires acc(r.f) && r.f > -38
+    ensures (r.f > 60) ==> result
+{ isGreaterOne(r.f) }
+
+
+method mPre(j: Int)
+{
+    var tmp : Bool
+    //:: ExpectedOutput(application.precondition:assertion.false)
+    tmp := isGreaterOne(j)
+}
+
+method mPre2(j: Int)
+{
+    var tmp : Bool
+    //:: ExpectedOutput(application.precondition:assertion.false)
+    tmp := @reveal() isGreaterOne(j)
+}
+
+method mPost()
+{
+    var tmp : Bool
+    tmp := isGreaterOne(70)
+    assert tmp
+}
+
+method mPost2()
+{
+    var tmp : Bool
+    tmp := @reveal() isGreaterOne(70)
+    assert tmp
+}
+
+method mDef(j: Int)
+    requires j > -50
+{
+    assume isGreaterOne(j)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert j > 1
+}
+
+method mDef2(j: Int)
+    requires j > -50
+{
+    assume @reveal() isGreaterOne(j)
+    assert j > 1
+}
+
+method mProveFun(j: Int)
+    requires j > 1
+{
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert isGreaterOne(j)
+}
+
+method mProveFun2(j: Int)
+    requires j > 1
+{
+    assert @reveal() isGreaterOne(j)
+}
+
+method mProveRevealed(j: Int)
+    requires j > -40
+{
+    assume isGreaterOne(j)
+    assert @reveal() isGreaterOne(j)
+    assert j > 1
+}
+
+method mProveRevealed2(j: Int)
+    requires j > -40
+{
+    assume isGreaterOne(j)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert j > 1
+}
+
+method mProveOpaque(j: Int)
+    requires j > -40
+{
+    assume @reveal() isGreaterOne(j)
+    assert isGreaterOne(j)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method mNestedFunc(r: Ref)
+    requires acc(r.f) && r.f > -20
+{
+    assume isGreaterOne2(r)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert r.f > 1
+}
+
+method mNestedFunc2(r: Ref)
+    requires acc(r.f) && r.f > -20
+{
+    assume @reveal() isGreaterOne2(r)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert r.f > 1
+}
+
+method mNestedFunc3(r: Ref)
+    requires acc(r.f) && r.f > -20
+{
+    assume isGreaterOne3(r)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert r.f > 1
+}
+
+method mNestedFunc4(r: Ref)
+    requires acc(r.f) && r.f > -20
+{
+    assume @reveal() isGreaterOne3(r)
+    assert r.f > 1
+}
+
+method mNestedFunc5(r: Ref)
+    requires acc(r.f) && r.f > -20
+{
+    assume isGreaterOne34(r)
+    assert r.f > 1
+}
+
+method mNestedFunc6(r: Ref)
+    requires acc(r.f) && r.f > -20
+{
+    assume isGreaterOne35(r)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert r.f > 1
+}
+
+function fac1(i: Int): Int
+{
+    i <= 1 ? 1 : i * fac1(i - 1)
+}
+
+@opaque()
+function fac2(i: Int): Int
+{
+    i <= 1 ? 1 : i * fac2(i - 1)
+}
+
+@opaque()
+function fac3(i: Int): Int
+{
+    i <= 1 ? 1 : i * (@reveal() fac3(i - 1))
+}
+
+method mFac1_1()
+{
+    var tmp : Int
+    tmp := fac1(3)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 6
+}
+
+method mFac1_2()
+{
+    var tmp : Int
+    tmp := fac1(3)
+    assert tmp == 3 * fac1(2)
+    assert tmp == 3 * 2 * fac1(1)
+    assert tmp == 6
+}
+
+method mFac2_1()
+{
+    var tmp : Int
+    tmp := fac2(3)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 6
+}
+
+method mFac2_2()
+{
+    var tmp : Int
+    tmp := fac2(3)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 3 * fac2(2)
+}
+
+method mFac2_3()
+{
+    var tmp : Int
+    tmp := @reveal() fac2(3)
+    assert tmp == 3 * @reveal() fac2(2)
+    assert tmp == 3 * 2 * @reveal() fac2(1)
+    assert tmp == 6
+}
+
+method mFac2_4()
+{
+    var tmp : Int
+    tmp := @reveal() fac2(3)
+    assert tmp == 3 * fac2(2)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 3 * 2 * fac2(1)
+}
+
+method mFac3_1()
+{
+    var tmp : Int
+    tmp := fac3(3)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 6
+}
+
+method mFac3_2()
+{
+    var tmp : Int
+    tmp := fac3(3)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 3 * fac3(2)
+}
+
+method mFac3_3()
+{
+    var tmp : Int
+    tmp := @reveal() fac3(3)
+    assert tmp == 3 * @reveal() fac3(2)
+    assert tmp == 3 * 2 * @reveal() fac3(1)
+    assert tmp == 6
+}
+
+method mFac3_4()
+{
+    var tmp : Int
+    tmp := @reveal() fac3(3)
+    assert tmp == 3 * fac3(2)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 3 * 2 * fac3(1)
+}
+
+method mFac3_5()
+{
+    var tmp : Int
+    tmp := @reveal() fac3(3)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert tmp == 6
+}
\ No newline at end of file

From 315fb2418b4776962ce99ce3469f5f3896ec787e Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 31 Oct 2023 13:52:13 +0100
Subject: [PATCH 42/61] Cleanup

---
 src/test/resources/all/functions/opaque.vpr | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/test/resources/all/functions/opaque.vpr b/src/test/resources/all/functions/opaque.vpr
index 401c9506b..59f3b595f 100644
--- a/src/test/resources/all/functions/opaque.vpr
+++ b/src/test/resources/all/functions/opaque.vpr
@@ -3,9 +3,6 @@
 
 field f: Int
 
-// use function and dont know def
-// recursive
-
 @opaque()
 function isGreaterOne(i: Int): Bool
     requires i > -60
@@ -43,7 +40,6 @@ function isGreaterOne32(r: Ref): Bool
 function isGreaterOne33(r: Ref): Bool
     requires acc(r.f)
     ensures (r.f > 60) ==> result
-    ensures result == r.f > 1
 //:: ExpectedOutput(application.precondition:assertion.false)
 { @reveal() isGreaterOne(r.f) }
 

From 94dfb40834f839e5be7fd449cc94d465beee394a Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 1 Nov 2023 16:11:46 +0100
Subject: [PATCH 43/61] Added test to ensure opaque functions do not have
 predicate triggers

---
 src/test/resources/all/functions/opaque.vpr | 45 +++++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/src/test/resources/all/functions/opaque.vpr b/src/test/resources/all/functions/opaque.vpr
index 59f3b595f..30cd2a690 100644
--- a/src/test/resources/all/functions/opaque.vpr
+++ b/src/test/resources/all/functions/opaque.vpr
@@ -289,4 +289,49 @@ method mFac3_5()
     tmp := @reveal() fac3(3)
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert tmp == 6
+}
+
+predicate P(x: Ref) {
+    acc(x.f)
+}
+
+@opaque()
+function funP(x: Ref): Int
+    requires P(x)
+{
+    unfolding P(x) in x.f
+}
+
+function funP2(x: Ref): Int
+    requires P(x)
+{
+    unfolding P(x) in x.f
+}
+
+method mFold(r: Ref)
+    requires acc(r.f)
+{
+    var tmp: Int
+    tmp := r.f
+    fold P(r)
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert funP(r) == tmp
+}
+
+method mFold2(r: Ref)
+    requires acc(r.f)
+{
+    var tmp: Int
+    tmp := r.f
+    fold P(r)
+    assert @reveal() funP(r) == tmp
+}
+
+method mFold3(r: Ref)
+    requires acc(r.f)
+{
+    var tmp: Int
+    tmp := r.f
+    fold P(r)
+    assert funP2(r) == tmp
 }
\ No newline at end of file

From 62dacc0f71d4204a6f6261ec12e008e40a13c91d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 1 Nov 2023 16:12:14 +0100
Subject: [PATCH 44/61] Moved test to annotation directory

---
 src/test/resources/all/{functions => annotation}/opaque.vpr | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename src/test/resources/all/{functions => annotation}/opaque.vpr (100%)

diff --git a/src/test/resources/all/functions/opaque.vpr b/src/test/resources/all/annotation/opaque.vpr
similarity index 100%
rename from src/test/resources/all/functions/opaque.vpr
rename to src/test/resources/all/annotation/opaque.vpr

From 34c754e962ffdd72565c5be8344b11c4ecbafbd2 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 8 Nov 2023 19:37:33 +0100
Subject: [PATCH 45/61] Adding test for Silicon issue #769

---
 src/test/resources/all/issues/silicon/0769.vpr | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0769.vpr

diff --git a/src/test/resources/all/issues/silicon/0769.vpr b/src/test/resources/all/issues/silicon/0769.vpr
new file mode 100644
index 000000000..3fa882feb
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0769.vpr
@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field values: Map[Int, Ref]
+
+field value: Int
+
+
+method main()
+{
+  var x: Ref
+  x := new(values)
+  x.values := Map()
+  //:: ExpectedOutput(assert.failed:map.key.contains)
+  assert x.values[1].value > 0
+  assert false
+}
\ No newline at end of file

From 165d0bf89b0bdfa535f15a9b6407c5f671752698 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 8 Nov 2023 21:28:39 +0100
Subject: [PATCH 46/61] Properly treating let-expressions when generating
 triggers (in a hopefully generic way)

---
 .../ast/utility/GenericTriggerGenerator.scala | 20 ++++++++++++++++---
 .../viper/silver/ast/utility/Triggers.scala   | 13 +++++++++++-
 src/test/resources/all/issues/silver/0751.vpr | 15 ++++++++++++++
 3 files changed, 44 insertions(+), 4 deletions(-)
 create mode 100644 src/test/resources/all/issues/silver/0751.vpr

diff --git a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
index 35f98c242..ec75b7c5e 100644
--- a/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
+++ b/src/main/scala/viper/silver/ast/utility/GenericTriggerGenerator.scala
@@ -165,6 +165,15 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
     val nestedBoundVars: Seq[Var] =
       deepCollect(toSearch){ case qe: Quantification => Quantification_vars(qe)}.flatten
 
+    val additionalRelevantVars: Seq[Var] = {
+      val additionalVarFinder = additionalRelevantVariables(vs, nestedBoundVars)
+      deepCollect(toSearch){
+        case n if additionalVarFinder.isDefinedAt(n) => additionalVarFinder(n)
+      }.flatten
+    }
+    val allRelevantVars = (vs ++ additionalRelevantVars).distinct
+    val modifyTriggers = modifyPossibleTriggers(allRelevantVars)
+
     /* Get all function applications */
     reduceTree(toSearch)((node: Node, results: Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]]) => node match {
       case possibleTrigger: PossibleTrigger if isPossibleTrigger(possibleTrigger) =>
@@ -187,7 +196,7 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
         processedArgs foreach (arg => visit(arg) {
           case v: Var =>
             if (nestedBoundVars.contains(v)) containsNestedBoundVars = true
-            if (vs.contains(v)) containedVars +:= v
+            if (allRelevantVars.contains(v)) containedVars +:= v
         })
 
         if (!containsNestedBoundVars && containedVars.nonEmpty)
@@ -195,7 +204,7 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
         else
           results.flatten
 
-      case e if modifyPossibleTriggers.isDefinedAt(e) => modifyPossibleTriggers.apply(e)(results)
+      case e if modifyTriggers.isDefinedAt(e) => modifyTriggers.apply(e)(results)
 
       case _ => results.flatten
     })
@@ -205,9 +214,14 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
    * Hook for clients to add more cases to getFunctionAppsContaining to modify the found possible triggers.
    * Used e.g. to wrap trigger expressions inferred from inside old-expression into old()
    */
-  def modifyPossibleTriggers: PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] =>
+  def modifyPossibleTriggers(relevantVars: Seq[Var]): PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] =>
     Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] = PartialFunction.empty
 
+  /*
+   * Hook for clients to identify additional variables which can be covered by triggers.
+   */
+  def additionalRelevantVariables(relevantVars: Seq[Var], varsToAvoid: Seq[Var]): PartialFunction[Node, Seq[Var]] = PartialFunction.empty
+
   /* Precondition: if vars is non-empty then every (f,vs) pair in functs
    * satisfies the property that vars and vs are not disjoint.
    *
diff --git a/src/main/scala/viper/silver/ast/utility/Triggers.scala b/src/main/scala/viper/silver/ast/utility/Triggers.scala
index 93b89e609..0516b0ffb 100644
--- a/src/main/scala/viper/silver/ast/utility/Triggers.scala
+++ b/src/main/scala/viper/silver/ast/utility/Triggers.scala
@@ -58,7 +58,7 @@ object Triggers {
       case _ => sys.error(s"Unexpected expression $e")
     }
 
-    override def modifyPossibleTriggers = {
+    override def modifyPossibleTriggers(relevantVars: Seq[LocalVar]) = {
       case ast.Old(_) => results =>
         results.flatten.map(t => {
           val exp = t._1
@@ -69,6 +69,17 @@ object Triggers {
           val exp = t._1
           (ast.LabelledOld(exp, l)(exp.pos, exp.info, exp.errT), t._2, t._3)
         })
+      case ast.Let(v, e, _) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          val coveredVars = t._2.filter(cv => cv != v.localVar) ++ relevantVars.filter(rv => e.contains(rv))
+          (exp.replace(v.localVar, e), coveredVars, t._3)
+        })
+    }
+
+    override def additionalRelevantVariables(relevantVars: Seq[LocalVar], varsToAvoid: Seq[LocalVar]): PartialFunction[Node, Seq[LocalVar]] = {
+      case ast.Let(v, e, _) if relevantVars.exists(v => e.contains(v)) && varsToAvoid.forall(v => !e.contains(v)) =>
+        Seq(v.localVar)
     }
   }
 
diff --git a/src/test/resources/all/issues/silver/0751.vpr b/src/test/resources/all/issues/silver/0751.vpr
new file mode 100644
index 000000000..a5c8bb0cd
--- /dev/null
+++ b/src/test/resources/all/issues/silver/0751.vpr
@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+method main() {
+    assume forall qvar: Int ::
+      let alias == (qvar) in
+        f_get(alias) == f_clamp() 
+    assert f_get(10) == 0
+}
+
+function f_get(idx: Int): Int
+
+
+function f_clamp(): Int
+  ensures result == 0
\ No newline at end of file

From c7ed3b916279e27f50433e226b0f9ee64372d1c0 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 8 Nov 2023 21:42:31 +0100
Subject: [PATCH 47/61] Slightly extended test to cover a case that needs an
 adjustment in Silicon

---
 src/test/resources/all/issues/silver/0751.vpr | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/test/resources/all/issues/silver/0751.vpr b/src/test/resources/all/issues/silver/0751.vpr
index a5c8bb0cd..b5469d8bb 100644
--- a/src/test/resources/all/issues/silver/0751.vpr
+++ b/src/test/resources/all/issues/silver/0751.vpr
@@ -4,12 +4,23 @@
 method main() {
     assume forall qvar: Int ::
       let alias == (qvar) in
-        f_get(alias) == f_clamp() 
+        f_get(alias) == f_clamp()
     assert f_get(10) == 0
 }
 
 function f_get(idx: Int): Int
 
 
+method main2() {
+    assume forall qvar: Int :: qvar > 0 ==>
+      let alias == (qvar) in
+        f_get2(alias) == f_clamp()
+    assert f_get2(10) == 0
+}
+
+function f_get2(idx: Int): Int
+    requires idx > -5
+
+
 function f_clamp(): Int
   ensures result == 0
\ No newline at end of file

From 4b50e1a368a84f142190ed40072da1515e327824 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 9 Nov 2023 15:15:37 +0100
Subject: [PATCH 48/61] Fixing precondition treatment in termination plugin
 proof methods

---
 .../transformation/ExpTransformer.scala       | 17 ++++
 .../transformation/FunctionCheck.scala        |  4 +-
 .../resources/all/issues/silicon/0768.vpr     | 89 +++++++++++++++++++
 3 files changed, 108 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/all/issues/silicon/0768.vpr

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
index e8b5fc324..cbd28af84 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
@@ -24,6 +24,23 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
    * @return a statement representing the expression.
    */
   def transformExp(e: Exp, c: ExpressionContext): Stmt = e match {
+    case And(fst, snd) =>
+      val fstStmt = transformExp(fst, c)
+      val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)
+      val assumeFalse = Inhale(FalseLit()())()
+      val inhaleFst = Inhale(fst)()
+      val inhaleFstStmt = if (fst.contains[InhaleExhaleExp]) {
+        c.conditionInEx match {
+          case Some(conditionVar) => If(conditionVar.localVar, Seqn(Seq(inhaleFst), Nil)(), Seqn(Seq(Inhale(fst.whenExhaling)()), Nil)())()
+          case None => inhaleFst
+        }
+      } else {
+        inhaleFst
+      }
+      val fstIf = If(nonDetVarDecl.localVar, Seqn(Seq(fstStmt, assumeFalse), Nil)(), Seqn(Seq(inhaleFstStmt), Nil)())(e.pos, e.info, e.errT)
+      val fstBlock = Seqn(Seq(fstIf), Seq(nonDetVarDecl))()
+      val sndStmt = transformExp(snd, c)
+      Seqn(Seq(fstBlock, sndStmt), Nil)()
     case CondExp(cond, thn, els) =>
       val condStmt = transformExp(cond, c)
       val thnStmt = transformExp(thn, c)
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
index 6fe62e5b9..5da623ade 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
@@ -85,7 +85,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
           .map(p => ViperStrategy.Slim({
             case Result(_) => resultVariable.localVar
           }, Traverse.BottomUp).execute[Exp](p))
-          .reduce((e, p) => And(e, p)())
+          .reduce((e, p) => And(e, p)(e.pos))
 
         val proofMethodBody: Stmt = {
           val stmt: Stmt = Simplifier.simplify(transformExp(posts, context))
@@ -111,7 +111,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         val context = FContext(f)
 
         // concatenate all pres
-        val pres = f.pres.reduce((e, p) => And(e, p)())
+        val pres = f.pres.reduce((e, p) => And(e, p)(e.pos))
 
         val proofMethodBody: Stmt = Simplifier.simplify(transformExp(pres, context))
 
diff --git a/src/test/resources/all/issues/silicon/0768.vpr b/src/test/resources/all/issues/silicon/0768.vpr
new file mode 100644
index 000000000..5a403626a
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0768.vpr
@@ -0,0 +1,89 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+domain block  {
+
+  function block_length(b: block): Int
+
+  function loc(b: block, i: Int): Ref
+
+  function loc_inv_1(r: Ref): block
+
+  function loc_inv_2(r: Ref): Int
+
+  axiom {
+    (forall b: block ::block_length(b) >= 0)
+  }
+
+  axiom {
+    (forall b: block, i: Int ::
+      { loc(b, i) }
+      loc_inv_1(loc(b, i)) == b && loc_inv_2(loc(b, i)) == i)
+  }
+}
+
+domain pointer  {
+
+  function pointer_of(b: block, offset: Int): pointer
+
+  function pointer_block(p: pointer): block
+
+  function pointer_offset(p: pointer): Int
+
+  axiom {
+    (forall p: pointer ::pointer_offset(p) >= 0 &&
+      pointer_offset(p) < block_length(pointer_block(p)))
+  }
+
+  axiom {
+    (forall b: block, offset: Int ::
+      { pointer_block(pointer_of(b, offset)), pointer_offset(pointer_of(b, offset)) }
+      pointer_block(pointer_of(b, offset)) == b &&
+      pointer_offset(pointer_of(b, offset)) == offset)
+  }
+}
+
+function ptr_deref(p: pointer): Ref
+  decreases
+{
+  loc(pointer_block(p), pointer_offset(p))
+}
+
+function ptr_add(p: pointer, offset: Int): pointer
+  requires 0 <= pointer_offset(p) + offset
+  requires pointer_offset(p) + offset < block_length(pointer_block(p))
+  decreases
+{
+  pointer_of(pointer_block(p), pointer_offset(p) + offset)
+}
+
+field ref: Ref
+field x: Int
+
+function inp_to_seq_2(inp: pointer, n: Int): Seq[Int]
+  requires n <=
+    block_length(pointer_block(inp)) -
+    pointer_offset(inp)
+  requires (forall i: Int ::
+      { ptr_deref(ptr_add(inp, i)).ref }
+      0 <= i && i < n ==>
+      acc(ptr_deref(ptr_add(inp, i)).ref, 1 *
+      write /
+      10))
+  requires (forall i: Int, j: Int ::0 <= i &&
+      i < n &&
+      0 <= j &&
+      j < n ==>
+      i != j ==>
+      ptr_deref(ptr_add((inp), i)).ref !=
+      ptr_deref(ptr_add((inp), j)).ref)
+  requires (forall i: Int ::
+      { ptr_deref(ptr_add(inp, i)).ref.x }
+      0 <= i && i < n ==>
+      acc(ptr_deref(ptr_add(inp, i)).ref.x, 1 *
+      write /
+      10))
+   decreases
+{
+  Seq[Int]()
+}
\ No newline at end of file

From 8ba970a684d9119eac4c8953db1ef9bb438a2cd2 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 10 Nov 2023 16:56:06 +0100
Subject: [PATCH 49/61] Test for Silicon issue #773

---
 .../resources/all/issues/silicon/0773.vpr     | 61 +++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 src/test/resources/all/issues/silicon/0773.vpr

diff --git a/src/test/resources/all/issues/silicon/0773.vpr b/src/test/resources/all/issues/silicon/0773.vpr
new file mode 100644
index 000000000..2ce6bdb12
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0773.vpr
@@ -0,0 +1,61 @@
+method test()
+{
+    label l0 invariant true
+    refute false
+    goto l0
+}
+
+method test2()
+{
+    label l0
+    refute false
+    goto l0
+}
+
+function pre(): Bool
+
+function needsPre(): Bool
+  requires pre()
+
+method test3()
+{
+    var tmp: Int
+    label l1
+    assume pre()
+    if (needsPre()) {
+        tmp := 3
+    } else {
+        tmp := 4
+    }
+    goto l1
+}
+
+method test3fail()
+{
+    var tmp: Int
+    label l1
+    //:: ExpectedOutput(application.precondition:assertion.false)
+    if (needsPre()) {
+        tmp := 3
+    } else {
+        tmp := 4
+    }
+    goto l1
+}
+
+
+method test4()
+{
+  {
+    label l0
+    {
+      var __plugin_refute_nondet1: Bool
+      if (__plugin_refute_nondet1) {
+        //:: ExpectedOutput(assert.failed:assertion.false)
+        assert false
+        inhale false
+      }
+    }
+    goto l0
+  }
+}
\ No newline at end of file

From f115905e76ee99c5510d5066823d37723a0e6bab Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 10 Nov 2023 17:57:15 +0100
Subject: [PATCH 50/61] Disable test that has been randomly non-terminating for
 a while

---
 .../resources/examples/quickselect/arrays_quickselect_rec.vpr   | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/test/resources/examples/quickselect/arrays_quickselect_rec.vpr b/src/test/resources/examples/quickselect/arrays_quickselect_rec.vpr
index 1748875ff..6d8db588f 100644
--- a/src/test/resources/examples/quickselect/arrays_quickselect_rec.vpr
+++ b/src/test/resources/examples/quickselect/arrays_quickselect_rec.vpr
@@ -1,6 +1,8 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
+//:: IgnoreFile(/carbon/issue/280/)
+
 
 /* https://en.wikipedia.org/wiki/Quickselect
  *

From 3c0e070be89e4cd786550a02660b3df0f6d6fbfe Mon Sep 17 00:00:00 2001
From: gauravpartha <gaurav.parthasarathy@inf.ethz.ch>
Date: Tue, 21 Nov 2023 14:03:42 +0100
Subject: [PATCH 51/61] fix issue number in ignored file for Carbon

---
 .../quickselect/arrays_quickselect_rec_index-shifting.vpr       | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/resources/examples/quickselect/arrays_quickselect_rec_index-shifting.vpr b/src/test/resources/examples/quickselect/arrays_quickselect_rec_index-shifting.vpr
index 5e20a6ddc..437cb66c2 100644
--- a/src/test/resources/examples/quickselect/arrays_quickselect_rec_index-shifting.vpr
+++ b/src/test/resources/examples/quickselect/arrays_quickselect_rec_index-shifting.vpr
@@ -1,7 +1,7 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/137/)
+//:: IgnoreFile(/carbon/issue/280/)
 
 /* This version differs from arrays_quickselect_rec.vpr in so far as the
  * permutation witness pw only covers the segment of the array that is being

From 7208338f5347845973f692458a64607ef663530f Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 28 Nov 2023 17:06:50 +0100
Subject: [PATCH 52/61] Restricted adapted encoding for inhaling to cases where
 it's appropriate

---
 .../transformation/ExpTransformer.scala       | 50 ++++++++++---------
 .../transformation/FunctionCheck.scala        | 12 ++---
 2 files changed, 33 insertions(+), 29 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
index cbd28af84..c771f084f 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala
@@ -19,13 +19,17 @@ import viper.silver.verifier.ConsistencyError
 trait ExpTransformer extends ProgramManager with ErrorReporter {
 
   /**
-   * Transforms an expression into a statement.
+   * Transforms an expression into a statement that checks the termination conditions for that expression.
+   * If inhaleExp is true, the expression is inhaled during the check.
    *
    * @return a statement representing the expression.
    */
-  def transformExp(e: Exp, c: ExpressionContext): Stmt = e match {
-    case And(fst, snd) =>
-      val fstStmt = transformExp(fst, c)
+  def transformExp(e: Exp, c: ExpressionContext, inhaleExp: Boolean): Stmt = e match {
+    case And(fst, snd) if inhaleExp =>
+      // Special case conjunctions s.t. we properly inhale the first expression before checking the second.
+      // This is necessary if fst contains e.g. a quantified permission, and snd is well-defined only if that quantified
+      // permission is available.
+      val fstStmt = transformExp(fst, c, inhaleExp)
       val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)
       val assumeFalse = Inhale(FalseLit()())()
       val inhaleFst = Inhale(fst)()
@@ -39,20 +43,20 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
       }
       val fstIf = If(nonDetVarDecl.localVar, Seqn(Seq(fstStmt, assumeFalse), Nil)(), Seqn(Seq(inhaleFstStmt), Nil)())(e.pos, e.info, e.errT)
       val fstBlock = Seqn(Seq(fstIf), Seq(nonDetVarDecl))()
-      val sndStmt = transformExp(snd, c)
+      val sndStmt = transformExp(snd, c, inhaleExp)
       Seqn(Seq(fstBlock, sndStmt), Nil)()
     case CondExp(cond, thn, els) =>
-      val condStmt = transformExp(cond, c)
-      val thnStmt = transformExp(thn, c)
-      val elsStmt = transformExp(els, c)
+      val condStmt = transformExp(cond, c, false)
+      val thnStmt = transformExp(thn, c, inhaleExp)
+      val elsStmt = transformExp(els, c, inhaleExp)
 
       val ifStmt = If(cond, Seqn(Seq(thnStmt), Nil)(), Seqn(Seq(elsStmt), Nil)())()
 
       val stmts = Seq(condStmt, ifStmt)
       Seqn(stmts, Nil)()
     case Unfolding(acc, unfBody) =>
-      val permCheck = transformExp(acc.perm, c)
-      val unfoldBody = transformExp(unfBody, c)
+      val permCheck = transformExp(acc.perm, c, false)
+      val unfoldBody = transformExp(unfBody, c, inhaleExp)
       // only unfold and fold if body contains something
       val (unfold, fold) = (Unfold(acc)(), Fold(acc)())
 
@@ -61,32 +65,32 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     case Applying(wand, body) =>
       // note that this case is untested -- it's not possible to write a function with an `applying` expression
       val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)
-      val bodyStmt = transformExp(body, c)
+      val bodyStmt = transformExp(body, c, inhaleExp)
       val killBranchStmt = Inhale(FalseLit()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
       val thnStmt = Seqn(Seq(Apply(wand)(e.pos, e.info, e.errT), bodyStmt, killBranchStmt), Nil)()
       val ifStmt = If(nonDetVarDecl.localVar, thnStmt, EmptyStmt)(e.pos, e.info, e.errT)
       Seqn(Seq(ifStmt), Seq(nonDetVarDecl))(e.pos, e.info, e.errT)
     case inex: InhaleExhaleExp =>
-      val inhaleStmt = transformExp(inex.in, c)
-      val exhaleStmt = transformExp(inex.ex, c)
+      val inhaleStmt = transformExp(inex.in, c, inhaleExp)
+      val exhaleStmt = transformExp(inex.ex, c, inhaleExp)
 
       c.conditionInEx match {
         case Some(conditionVar) => If(conditionVar.localVar, Seqn(Seq(inhaleStmt), Nil)(), Seqn(Seq(exhaleStmt), Nil)())()
         case None => Seqn(Seq(inhaleStmt, exhaleStmt), Nil)()
       }
     case letExp: Let =>
-      val expressionStmt = transformExp(letExp.exp, c)
+      val expressionStmt = transformExp(letExp.exp, c, false)
       val localVarDecl = letExp.variable
 
       val inhaleEq = Inhale(EqCmp(localVarDecl.localVar, letExp.exp)())()
 
-      val bodyStmt = transformExp(letExp.body, c)
+      val bodyStmt = transformExp(letExp.body, c, inhaleExp)
 
       Seqn(Seq(expressionStmt, inhaleEq, bodyStmt), Seq(localVarDecl))()
 
     case b: BinExp =>
-      val left = transformExp(b.left, c)
-      val right = transformExp(b.right, c)
+      val left = transformExp(b.left, c, inhaleExp)
+      val right = transformExp(b.right, c, inhaleExp)
 
       // Short circuit evaluation
       val pureLeft: Exp = toPureBooleanExp(c).execute(b.left)
@@ -111,21 +115,21 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
     case _: LocationAccess => EmptyStmt
 
     case ap: AccessPredicate =>
-      val check = transformExp(ap.perm, c)
+      val check = transformExp(ap.perm, c, false)
       val inhale = Inhale(ap)(ap.pos)
       Seqn(Seq(check, inhale), Nil)()
     case fa: Forall =>
       // we turn the quantified variables into local variables with arbitrary value and show that the expression holds
       // for arbitrary values, which is similar to a forall introduction
       val (localDeclMapping, transformedExp) = substituteWithFreshVars(fa.variables, fa.exp)
-      val expressionStmt = transformExp(transformedExp, c)
+      val expressionStmt = transformExp(transformedExp, c, inhaleExp)
       Seqn(Seq(expressionStmt), localDeclMapping.map(_._2))(fa.pos, fa.info, fa.errT)
     case fp: ForPerm =>
       // let's pick arbitrary values for the quantified variables and check the body given that the current heap has
       // sufficient permissions
       val (localDeclMapping, transformedExp) = substituteWithFreshVars(fp.variables, fp.exp)
       val transformedRes = applySubstitution(localDeclMapping, fp.resource)
-      val expressionStmt = transformExp(transformedExp, c)
+      val expressionStmt = transformExp(transformedExp, c, inhaleExp)
       val killBranchStmt = Inhale(FalseLit()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
       val thnStmt = Seqn(Seq(expressionStmt, killBranchStmt), Nil)(e.pos, e.info, e.errT)
       val ifCond = GtCmp(CurrentPerm(transformedRes)(e.pos, e.info, e.errT), NoPerm()(e.pos, e.info, e.errT))(e.pos, e.info, e.errT)
@@ -137,15 +141,15 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
       // we can't use an assume statement at this point because the `assume`s have already been rewritten
       // furthermore, Viper only allows pure existentially quantified expressions
       val inhaleWitnesses = Inhale(transformedExp)(ex.pos, ex.info, ex.errT)
-      val expressionStmt = transformExp(transformedExp, c)
+      val expressionStmt = transformExp(transformedExp, c, inhaleExp)
       Seqn(Seq(inhaleWitnesses, expressionStmt), localDeclMapping.map(_._2))(ex.pos, ex.info, ex.errT)
     case fa: FuncLikeApp =>
-      val argStmts = fa.args.map(transformExp(_, c))
+      val argStmts = fa.args.map(transformExp(_, c, false))
       Seqn(argStmts, Nil)()
     case e: ExtensionExp => reportUnsupportedExp(e)
 
     case _ =>
-      val sub = e.subExps.map(transformExp(_, c))
+      val sub = e.subExps.map(transformExp(_, c, false))
       Seqn(sub, Nil)()
   }
 
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
index 5da623ade..cb028f3ac 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/FunctionCheck.scala
@@ -53,7 +53,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         val context = FContext(f)
 
         val proofMethodBody: Stmt = {
-          val stmt: Stmt = Simplifier.simplify(transformExp(f.body.get, context))
+          val stmt: Stmt = Simplifier.simplify(transformExp(f.body.get, context, false))
           if (requireNestedInfo) {
             addNestedPredicateInformation.execute(stmt)
           } else {
@@ -88,7 +88,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
           .reduce((e, p) => And(e, p)(e.pos))
 
         val proofMethodBody: Stmt = {
-          val stmt: Stmt = Simplifier.simplify(transformExp(posts, context))
+          val stmt: Stmt = Simplifier.simplify(transformExp(posts, context, false))
           if (requireNestedInfo) {
             addNestedPredicateInformation.execute(stmt)
           } else {
@@ -113,7 +113,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         // concatenate all pres
         val pres = f.pres.reduce((e, p) => And(e, p)(e.pos))
 
-        val proofMethodBody: Stmt = Simplifier.simplify(transformExp(pres, context))
+        val proofMethodBody: Stmt = Simplifier.simplify(transformExp(pres, context, true))
 
         if (proofMethodBody != EmptyStmt) {
           val proofMethod = Method(proofMethodName, f.formalArgs, Nil, Nil, Nil,
@@ -136,12 +136,12 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
    *
    * @return a statement representing the expression
    */
-  override def transformExp(e: Exp, c: ExpressionContext): Stmt = (e, c) match {
+  override def transformExp(e: Exp, c: ExpressionContext, inhaleExp: Boolean): Stmt = (e, c) match {
     case (functionCall: FuncApp, context: FunctionContext @unchecked) =>
       val stmts = collection.mutable.ArrayBuffer[Stmt]()
 
       // check the arguments
-      val termChecksOfArgs: Seq[Stmt] = functionCall.getArgs map (a => transformExp(a, context))
+      val termChecksOfArgs: Seq[Stmt] = functionCall.getArgs map (a => transformExp(a, context, false))
       stmts.appendAll(termChecksOfArgs)
 
       getFunctionDecreasesSpecification(context.functionName).tuple match {
@@ -218,7 +218,7 @@ trait FunctionCheck extends ProgramManager with DecreasesCheck with ExpTransform
         // should not happen
       }
       Seqn(stmts.toSeq, Nil)()
-    case _ => super.transformExp(e, c)
+    case _ => super.transformExp(e, c, inhaleExp)
   }
 
   // context creator

From 3f64dcfd4dc1a8d36f0e29cec8bae7d99f4eea06 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 28 Nov 2023 17:12:28 +0100
Subject: [PATCH 53/61] Extended test

---
 .../resources/all/issues/silicon/0768.vpr     | 24 ++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/test/resources/all/issues/silicon/0768.vpr b/src/test/resources/all/issues/silicon/0768.vpr
index 5a403626a..3f055698c 100644
--- a/src/test/resources/all/issues/silicon/0768.vpr
+++ b/src/test/resources/all/issues/silicon/0768.vpr
@@ -86,4 +86,26 @@ function inp_to_seq_2(inp: pointer, n: Int): Seq[Int]
    decreases
 {
   Seq[Int]()
-}
\ No newline at end of file
+}
+
+// Regression test for a bug in the original fix:
+
+adt tree {
+    leaf(value: Int)
+    node(left: tree, right: tree)
+}
+
+function leafCount(t: tree): Int
+    decreases 1
+{
+    id(t.isleaf && t.isleaf ?
+        (1) :
+        //:: ExpectedOutput(termination.failed:tuple.false)
+        (leafCount(t.left) + leafCount(t.right)))
+}
+
+function id(i: Int): Int
+    decreases 0
+{
+    i
+}

From f9e546770ca39b8b67617a84f5686601ba16c0ee Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 30 Nov 2023 16:52:09 +0100
Subject: [PATCH 54/61] No longer substituting Int as default for unconstrained
 type variables inside domains

---
 .../scala/viper/silver/parser/ParseAst.scala  | 14 +++++++--
 .../scala/viper/silver/parser/Resolver.scala  | 30 ++++++++++++++++---
 src/test/resources/all/issues/silver/0236.vpr | 19 ++++++++++++
 3 files changed, 57 insertions(+), 6 deletions(-)
 create mode 100644 src/test/resources/all/issues/silver/0236.vpr

diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 09b1bc8a7..83a3482be 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -321,6 +321,7 @@ object PTypeVar {
   }
 
   val sep = "#"
+  val domainNameSep = "%"
 
   //TODO: do this properly
   def isFreePTVName(s: String) = s.contains(sep)
@@ -342,9 +343,18 @@ object PTypeVar {
     freshTypeSubstitution(tvs map (tv => tv.domain.name))
   }
 
-  def freshTypeSubstitution(tvns: Seq[String]): PTypeRenaming = {
+  def freshTypeSubstitution(tvns: Seq[String], domainName: Option[String] = None): PTypeRenaming = {
     val ind = lastIndex.getAndIncrement()
-    new PTypeRenaming((tvns map (tv => tv -> getFreshName(tv, ind))).toMap)
+    new PTypeRenaming((tvns map (tv => {
+      val tvName = domainName match {
+        case Some(dn) =>
+          // Choose a name for the type variable that contains the domain name.
+          // This enables us to choose a useful default in case the type variable is unconstrained.
+          dn + domainNameSep + tv
+        case None => tv
+      }
+      tv -> getFreshName(tvName, ind)
+    })).toMap)
   }
 }
 
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index f243a5677..7720a64f3 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -492,9 +492,31 @@ case class TypeChecker(names: NameAnalyser) {
 
   def ground(exp: PExp, pts: PTypeSubstitution): PTypeSubstitution = {
     pts.m.flatMap(kv => kv._2.freeTypeVariables &~ pts.m.keySet).foldLeft(pts)((ts, fv) => {
-      messages ++= FastMessaging.message(exp,
-        s"Unconstrained type parameter, substituting default type ${PTypeSubstitution.defaultType}.", error = false)
-      ts.add(PTypeVar(fv), PTypeSubstitution.defaultType).toOption.get
+      var chosenType: PType = PTypeSubstitution.defaultType
+      curMember match {
+        case ax: PAxiom if ax.parent.exists(p => p.isInstanceOf[PDomain]) =>
+          // If we are inside the domain that defines the type variable, then we choose the type variable itself
+          // as the default.
+          val domain = ax.parent.get.asInstanceOf[PDomain]
+          // The name pf domain function application type variables has the form
+          // domainName + PTypeVar.domainNameSep + typeVarName + PTypeVar.sep + index
+          if (fv.startsWith(domain.idndef.name + PTypeVar.domainNameSep)) {
+            var tvName = fv.substring(domain.idndef.name.length + 1)
+            if (tvName.contains(PTypeVar.sep)) {
+              tvName = tvName.substring(0, tvName.indexOf(PTypeVar.sep))
+              if (domain.typVars.exists(tv => tv.idndef.name == tvName)) {
+                // The type variable refers to an actual type variable of the current domain.
+                chosenType = PTypeVar(tvName)
+              }
+            }
+          }
+        case _ =>
+      }
+      if (chosenType == PTypeSubstitution.defaultType) {
+        messages ++= FastMessaging.message(exp,
+          s"Unconstrained type parameter, substituting default type ${PTypeSubstitution.defaultType}.", error = false)
+      }
+      ts.add(PTypeVar(fv), chosenType).toOption.get
     })
   }
 
@@ -642,7 +664,7 @@ case class TypeChecker(names: NameAnalyser) {
 
                         case pdf@PDomainFunction(_, _, _, _, _) =>
                           val domain = names.definition(curMember)(pdf.domainName).get.asInstanceOf[PDomain]
-                          val fdtv = PTypeVar.freshTypeSubstitution((domain.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables
+                          val fdtv = PTypeVar.freshTypeSubstitution((domain.typVars map (tv => tv.idndef.name)).distinct, Some(domain.idndef.name)) //fresh domain type variables
                           pfa.domainTypeRenaming = Some(fdtv)
                           pfa._extraLocalTypeVariables = (domain.typVars map (tv => PTypeVar(tv.idndef.name))).toSet
                           extraReturnTypeConstraint = explicitType
diff --git a/src/test/resources/all/issues/silver/0236.vpr b/src/test/resources/all/issues/silver/0236.vpr
new file mode 100644
index 000000000..ae595b884
--- /dev/null
+++ b/src/test/resources/all/issues/silver/0236.vpr
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+domain Option[T] {
+  axiom ax_Option_None_discr {
+    Option_discr(Option_None()) == 0
+  }
+  function Option_discr(Option[T]): Int
+  function Option_None(): Option[T]
+  function Option_Some(T): Option[T]
+}
+
+method m() {
+    assert Option_discr((Option_None(): Option[Bool])) == 0;
+    assert Option_discr((Option_None(): Option[Ref])) == 0;
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert Option_discr((Option_None(): Option[Perm])) == 1;
+}
\ No newline at end of file

From fd75485f67074d0d17bea7bd94f30765b0cc9320 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 12 Dec 2023 20:47:28 +0100
Subject: [PATCH 55/61] Checking if current scope is contained in an axiom, not
 just if it is directly an axiom

---
 .../scala/viper/silver/parser/Resolver.scala    |  9 +++++++--
 src/test/resources/all/issues/silver/0236.vpr   | 17 +++++++++++++++++
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index 7720a64f3..7d508f91a 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -490,11 +490,16 @@ case class TypeChecker(names: NameAnalyser) {
     Right(pss)
   }
 
+  def getParentAxiom(n: PNode): Option[PAxiom] = n match {
+    case a: PAxiom => Some(a)
+    case _ => n.parent.flatMap(getParentAxiom)
+  }
+
   def ground(exp: PExp, pts: PTypeSubstitution): PTypeSubstitution = {
     pts.m.flatMap(kv => kv._2.freeTypeVariables &~ pts.m.keySet).foldLeft(pts)((ts, fv) => {
       var chosenType: PType = PTypeSubstitution.defaultType
-      curMember match {
-        case ax: PAxiom if ax.parent.exists(p => p.isInstanceOf[PDomain]) =>
+      getParentAxiom(curMember) match {
+        case Some(ax: PAxiom) if ax.parent.exists(p => p.isInstanceOf[PDomain]) =>
           // If we are inside the domain that defines the type variable, then we choose the type variable itself
           // as the default.
           val domain = ax.parent.get.asInstanceOf[PDomain]
diff --git a/src/test/resources/all/issues/silver/0236.vpr b/src/test/resources/all/issues/silver/0236.vpr
index ae595b884..43de06c18 100644
--- a/src/test/resources/all/issues/silver/0236.vpr
+++ b/src/test/resources/all/issues/silver/0236.vpr
@@ -16,4 +16,21 @@ method m() {
 
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert Option_discr((Option_None(): Option[Perm])) == 1;
+}
+
+
+domain Option2[T] {
+  axiom ax_Option2_None_discr {
+    forall o: Option2[T] :: Option2_discr(o) >= 0 && Option2_discr(Option2_None()) == 0
+  }
+  function Option2_discr(Option2[T]): Int
+  function Option2_None(): Option2[T]
+  function Option2_Some(T): Option2[T]
+}
+
+method m2() {
+    assert Option2_discr(Option2_None()) == 0
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert Option2_discr(Option2_None()) == 1
 }
\ No newline at end of file

From c8b2f67869c9e69c3d5984fead4f113bece45803 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 12 Dec 2023 20:54:10 +0100
Subject: [PATCH 56/61] Fixed extended test

---
 src/test/resources/all/issues/silver/0236.vpr | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/test/resources/all/issues/silver/0236.vpr b/src/test/resources/all/issues/silver/0236.vpr
index 43de06c18..0adbe35be 100644
--- a/src/test/resources/all/issues/silver/0236.vpr
+++ b/src/test/resources/all/issues/silver/0236.vpr
@@ -2,7 +2,7 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 domain Option[T] {
-  axiom ax_Option_None_discr {
+  axiom  {
     Option_discr(Option_None()) == 0
   }
   function Option_discr(Option[T]): Int
@@ -29,8 +29,8 @@ domain Option2[T] {
 }
 
 method m2() {
-    assert Option2_discr(Option2_None()) == 0
+    assert Option2_discr((Option2_None(): Option2[Bool])) == 0
 
     //:: ExpectedOutput(assert.failed:assertion.false)
-    assert Option2_discr(Option2_None()) == 1
+    assert Option2_discr((Option2_None(): Option2[Bool])) == 1
 }
\ No newline at end of file

From 1e642a3d540c72fcfcea44a2a53ed879fe67200c Mon Sep 17 00:00:00 2001
From: Lea Salome Brugger <leasalome.brugger@inf.ethz.ch>
Date: Mon, 8 Jan 2024 15:40:59 +0100
Subject: [PATCH 57/61] Add unreachable statement

---
 .../smoke/UnreachableASTExtension.scala       | 19 +++++++++++++++++++
 .../smoke/UnreachablePASTExtension.scala      | 19 +++++++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala
 create mode 100644 src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala

diff --git a/src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala
new file mode 100644
index 000000000..4ca3d226a
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachableASTExtension.scala
@@ -0,0 +1,19 @@
+// 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.silver.plugin.standard.smoke
+
+import viper.silver.ast._
+import viper.silver.ast.pretty.FastPrettyPrinter.text
+import viper.silver.ast.pretty.PrettyPrintPrimitives
+
+case class Unreachable()(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt {
+
+  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = text("unreachable")
+
+  override def extensionSubnodes: Seq[Node] = Seq()
+}
+
diff --git a/src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala
new file mode 100644
index 000000000..2b1e996c1
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/smoke/UnreachablePASTExtension.scala
@@ -0,0 +1,19 @@
+// 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.silver.plugin.standard.smoke
+
+import viper.silver.ast.{Position, Stmt}
+import viper.silver.parser._
+
+case class PUnreachable()(val pos: (Position, Position)) extends PExtender with PStmt {
+  override val getSubnodes: Seq[PNode] = Seq()
+  override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
+    None
+  }
+
+  override def translateStmt(t: Translator): Stmt = Unreachable()(t.liftPos(this))
+}

From cb8caaeb85ee0730e28cb6eeb113b7721010f2f5 Mon Sep 17 00:00:00 2001
From: Lea Salome Brugger <leasalome.brugger@inf.ethz.ch>
Date: Mon, 8 Jan 2024 15:41:34 +0100
Subject: [PATCH 58/61] Implement smoke detection

---
 .../plugin/standard/refute/RefuteErrors.scala |   6 +-
 .../plugin/standard/refute/RefutePlugin.scala |   2 +-
 .../standard/smoke/SmokeDetectionPlugin.scala | 235 ++++++++++++++++++
 3 files changed, 241 insertions(+), 2 deletions(-)
 create mode 100644 src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala

diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
index e3642b52a..8901fb213 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
@@ -6,6 +6,8 @@
 
 package viper.silver.plugin.standard.refute
 
+import viper.silver.ast.FalseLit
+import viper.silver.plugin.standard.smoke.SmokeDetectionInfo
 import viper.silver.verifier._
 
 sealed abstract class RefuteError extends ExtensionAbstractVerificationError
@@ -13,7 +15,9 @@ sealed abstract class RefuteErrorReason extends ExtensionAbstractErrorReason
 
 case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends RefuteError {
   override val id = "refute.failed"
-  override val text = "Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)."
+  override val text: String = if (offendingNode.exp.isInstanceOf[FalseLit] && offendingNode.info.getUniqueInfo[SmokeDetectionInfo].isDefined)
+    "Smoke detection: False could be proven here (which should never hold)." else
+    "Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)."
 
   override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): RefuteFailed =
     RefuteFailed(this.offendingNode, this.reason, this.cached)
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index 131fb58cc..268608e66 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -56,7 +56,7 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
             If(nonDetLocalVarDecl.localVar,
               Seqn(Seq(
                 Assert(exp)(r.pos, RefuteInfo(r)),
-                Inhale(BoolLit(false)(r.pos))(r.pos)
+                Inhale(BoolLit(false)(r.pos))(r.pos, Synthesized)
               ), Seq())(r.pos),
               Seqn(Seq(), Seq())(r.pos))(r.pos)
           ),
diff --git a/src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala b/src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala
new file mode 100644
index 000000000..354418315
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala
@@ -0,0 +1,235 @@
+package viper.silver.plugin.standard.smoke
+
+import fastparse.P
+import viper.silver.ast._
+import viper.silver.ast.utility.ViperStrategy
+import viper.silver.cfg.silver.SilverCfg
+import viper.silver.cfg.silver.SilverCfg.SilverBlock
+import viper.silver.parser.FastParser
+import viper.silver.plugin.standard.refute.Refute
+import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
+
+import scala.annotation.unused
+import scala.collection.mutable.ListBuffer
+
+class SmokeDetectionPlugin(@unused reporter: viper.silver.reporter.Reporter,
+                           @unused logger: ch.qos.logback.classic.Logger,
+                           @unused config: viper.silver.frontend.SilFrontendConfig,
+                           fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
+
+  import fp.{FP, ParserExtension, keyword}
+
+  /** Keyword used to define `unreachable` statement. */
+  private val unreachableKeyword: String = "unreachable"
+
+  /** Parser for `unreachable` statements. */
+  def unreachable[$: P]: P[PUnreachable] =
+    FP(keyword(unreachableKeyword)).map { case (pos, _) => PUnreachable()(pos) }
+
+  /** Add `unreachable` to the parser. */
+  override def beforeParse(input: String, isImported: Boolean): String = {
+    // Add new keyword
+    ParserExtension.addNewKeywords(Set[String](unreachableKeyword))
+    // Add new parser to the precondition
+    ParserExtension.addNewStmtAtEnd(unreachable(_))
+    input
+  }
+
+  override def beforeVerify(input: Program): Program = {
+    var refuteId = 0
+
+    // Add `refute false` at end of each method body
+    val transformedMethods = input.methods.map(method => {
+      val bodyWithRefute = if (method.body.isEmpty) method.body else
+        Option(Seqn(method.body.toSeq :+ refuteFalse(method.pos, refuteId), Seq())(method.pos))
+
+      Method(method.name, method.formalArgs, method.formalReturns, method.pres,
+        method.posts, bodyWithRefute)(method.pos, method.info, method.errT)
+    })
+
+    // Add `refute false` after each inhale, at end of each loop body, at end of each if/else branch and before each goto
+    val methodsWithRefutes = transformedMethods.map(method => {
+      ViperStrategy.Slim({
+        case i@Inhale(expr) if i.info.getUniqueInfo[Synthesized.type].isEmpty =>
+          refuteId += 1
+          appendRefuteFalse(Inhale(expr)(i.pos, Synthesized), i.pos, refuteId)
+        case w@While(cond, invs, body) =>
+          refuteId += 1
+          While(cond, invs, appendRefuteFalse(body, body.pos, refuteId))(w.pos)
+        case i@If(cond, thn, els) =>
+          var thnWithRefute: Seqn = thn
+          var elsWithRefute: Seqn = els
+
+          if (thn.ss.nonEmpty) {
+            refuteId += 1
+            thnWithRefute = appendRefuteFalse(thn, thn.pos, refuteId)
+          }
+
+          if (els.ss.nonEmpty) {
+            refuteId += 1
+            elsWithRefute = appendRefuteFalse(els, els.pos, refuteId)
+          }
+
+          If(cond, thnWithRefute, elsWithRefute)(i.pos)
+        case g@Goto(target) if g.info.getUniqueInfo[Synthesized.type].isEmpty =>
+          refuteId += 1
+          Seqn(Seq(refuteFalse(g.pos, refuteId), Goto(target)(g.pos, Synthesized)), Seq())(g.pos)
+      }).execute[Method](method)
+    })
+
+    // Remove all `refute false` statements which are inside of control-flow branch marked as unreachable
+    val methodsWithoutUnreachableRefutes = methodsWithRefutes.map(method => {
+      val cfg = method.toCfg(simplify = false)
+      val result = collectRefutesToKeep(cfg)
+
+      ViperStrategy.Slim({
+        case r@Refute(_) =>
+          val info = r.info.getUniqueInfo[SmokeDetectionInfo]
+
+          if (info.isDefined &&
+            !result._1.contains(info.get.id) && // not marked reachable
+            result._2.contains(info.get.id)) { // actually considered when traversing CFG
+            Seqn(Seq(), Seq())(r.pos) // remove refute statement
+          } else {
+            r
+          }
+        case u@Unreachable() =>
+          Seqn(Seq(), Seq())(u.pos)
+      }).execute[Method](method)
+    })
+
+    Program(input.domains, input.fields, input.functions, input.predicates, methodsWithoutUnreachableRefutes,
+      input.extensions)(input.pos, input.info, input.errT)
+  }
+
+  /**
+   * Construct a [[Seqn]] consisting of `stmt` followed by a `refute false` statement with position `pos`.
+   * The `Refute` instance will have the ID `refuteId`.
+   *
+   * @param stmt     the statement at the beginning of the sequence
+   * @param pos      the position of the resulting [[Seqn]] instance
+   * @param refuteId the ID of the `refute false` statement at the end of the sequence
+   * @return a [[Seqn]] instance consisting of `stmt` and a `refute false` statement
+   */
+  private def appendRefuteFalse(stmt: Stmt, pos: Position, refuteId: Int): Seqn = {
+    Seqn(Seq(stmt, refuteFalse(pos, refuteId)), Seq())(pos)
+  }
+
+  /**
+   * Construct a `refute false` statement with position `pos` and ID `id`.
+   *
+   * @param pos the position of the resulting [[Refute]] instance
+   * @param id  the ID of the `refute false` statement
+   * @return a [[Refute]] instance with with the `exp` set to `false` and the given position and ID
+   */
+  private def refuteFalse(pos: Position, id: Int): Refute = {
+    Refute(FalseLit()(pos))(pos, SmokeDetectionInfo(id))
+  }
+
+  /**
+   * Construct a list of the IDs of all `refute false` statements that are not marked unreachable.
+   *
+   * @param cfg the control-flow graph of a method
+   * @return a list of the IDs of the reachable `refute false` statements and a list of the IDs of the `refute false`
+   *         statements that were encountered when traversing the control-flow graph
+   */
+  private def collectRefutesToKeep(cfg: SilverCfg): (List[Int], List[Int]) = {
+    val refutesToKeep = ListBuffer[Int]()
+    val seenRefutes = ListBuffer[Int]()
+    collectRefutesToKeepUntilExit(cfg, cfg.entry, cfg.exit.toSeq, ListBuffer[SilverBlock](),
+      refutesToKeep, seenRefutes, unreachable = false)
+    (refutesToKeep.toList, seenRefutes.toList)
+  }
+
+  /**
+   * Recursively construct a list of the IDs of all `refute false` statements that are not marked as unreachable on the
+   * path from the node `current` to one of the nodes in `exits` in the control-flow graph `cfg`.
+   *
+   * @param cfg           the control-flow graph
+   * @param current       the currently considered node in the control-flow graph
+   * @param exits         a list of potential exit nodes of the currently considered subgraph
+   * @param seen          a list of all nodes of the control-flow graph that have already been visited
+   * @param refutesToKeep the list of the IDs of all `refute false` statements which are not on an unreachable path
+   * @param seenRefutes the list of the IDs of all `refute false` statements that were already considered
+   * @param unreachable   indicates whether the current node is on a path marked as unreachable
+   * @return `true` if some part of the path from the `current` node to one of the `exits` is unreachable, otherwise `false`
+   */
+  private def collectRefutesToKeepUntilExit(cfg: SilverCfg,
+                                            current: SilverBlock,
+                                            exits: Seq[SilverBlock],
+                                            seen: ListBuffer[SilverBlock],
+                                            refutesToKeep: ListBuffer[Int],
+                                            seenRefutes: ListBuffer[Int],
+                                            unreachable: Boolean): Boolean = {
+    seen += current
+    val elements = current.elements
+
+    var unreachableSuccessors = unreachable
+
+    for (elem <- elements) {
+      val leftElem = elem.left.getOrElse(null)
+
+      leftElem match {
+        case _: Unreachable =>
+          // Encountered `unreachable` statement -> successors of current node are unreachable
+          unreachableSuccessors = true
+        case refute: Refute if refute.exp.isInstanceOf[FalseLit] =>
+          // Encountered `refute false` statement -> add ID to list if it is reachable
+          val info = refute.info.getUniqueInfo[SmokeDetectionInfo]
+
+          if (info.isDefined) {
+            val id = info.get.id
+
+            if (!unreachableSuccessors) {
+              refutesToKeep += id
+            }
+
+            seenRefutes += id
+          }
+        case _ =>
+      }
+    }
+
+    if (exits.contains(current)) {
+      // Considered whole path
+      return unreachableSuccessors
+    }
+
+    val successors = cfg.successors(current).filter(s => !seen.contains(s))
+    val joinPointMap = cfg.joinPoints
+
+    if (joinPointMap.contains(current)) {
+      // Current node is branch point
+      val joinPoint = joinPointMap(current)
+      val joinPointPredecessors = cfg.predecessors(joinPoint)
+      var allBranchesUnreachable = true
+
+      for (elem <- successors) {
+        val unreachableBranch = collectRefutesToKeepUntilExit(cfg, elem, joinPointPredecessors, seen,
+          refutesToKeep, seenRefutes, unreachableSuccessors)
+        if (!unreachableBranch) {
+          allBranchesUnreachable = false
+        }
+      }
+
+      // If all paths from the branch point to the join point contain an `unreachable` statement, the code following
+      // the joint point (including the join point) is also unreachable.
+      return collectRefutesToKeepUntilExit(cfg, joinPoint, exits, seen, refutesToKeep, seenRefutes, allBranchesUnreachable)
+    }
+
+    // Current node is no branch point -> collect Refute IDs for successor node
+    successors.forall(s => collectRefutesToKeepUntilExit(cfg, s, exits, seen, refutesToKeep, seenRefutes, unreachableSuccessors))
+  }
+}
+
+/**
+ * An info used to mark AST nodes (more specifically, `refute false` statements) as used in smoke detection,
+ * also assigning a unique identifier to it.
+ *
+ * @param id the ID of the node
+ */
+case class SmokeDetectionInfo(id: Int) extends Info {
+  override def comment: Seq[String] = Seq(s"`refute false` #$id")
+
+  override def isCached: Boolean = false
+}

From c0156dc3ffacba1d46affc0d69d739bbaf830782 Mon Sep 17 00:00:00 2001
From: Lea Salome Brugger <leasalome.brugger@inf.ethz.ch>
Date: Mon, 8 Jan 2024 15:42:12 +0100
Subject: [PATCH 59/61] Add frontend option to enable smoke detection

---
 .../silver/frontend/SilFrontEndConfig.scala   |  7 +++
 .../viper/silver/frontend/SilFrontend.scala   | 58 ++++++++++++-------
 2 files changed, 43 insertions(+), 22 deletions(-)

diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
index b837c5aed..4dd374f3a 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
@@ -82,6 +82,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     hidden = true
   )
 
+  val enableSmokeDetection = opt[Boolean]("enableSmokeDetection",
+    descr = "Enable smoke detection (if enabled, refute false statements are inserted in the code in order to detect unsound specifications).",
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
   val disableDefaultPlugins = opt[Boolean]("disableDefaultPlugins",
     descr = "Deactivate all default plugins.",
     default = Some(false),
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index a2ee386f0..5ce0cefa2 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -31,20 +31,21 @@ trait SilFrontend extends DefaultFrontend {
    */
   object ApplicationExitReason extends Enumeration {
     type PreVerificationFailureReasons = Value
-    val UNKNOWN_EXIT_REASON            = Value(-2)
-    val NOTHING_TO_BE_DONE             = Value(-1)
-    val VERIFICATION_SUCCEEDED         = Value( 0) // POSIX standard
-    val VERIFICATION_FAILED            = Value( 1)
-    val COMMAND_LINE_ARGS_PARSE_FAILED = Value( 2)
-    val ISSUE_WITH_PLUGINS             = Value( 3)
-    val SYSTEM_DEPENDENCY_UNSATISFIED  = Value( 4)
+    val UNKNOWN_EXIT_REASON = Value(-2)
+    val NOTHING_TO_BE_DONE = Value(-1)
+    val VERIFICATION_SUCCEEDED = Value(0) // POSIX standard
+    val VERIFICATION_FAILED = Value(1)
+    val COMMAND_LINE_ARGS_PARSE_FAILED = Value(2)
+    val ISSUE_WITH_PLUGINS = Value(3)
+    val SYSTEM_DEPENDENCY_UNSATISFIED = Value(4)
   }
 
   protected var _appExitReason: ApplicationExitReason.Value = ApplicationExitReason.UNKNOWN_EXIT_REASON
+
   def appExitCode: Int = _appExitReason.id
 
   protected def specifyAppExitCode(): Unit = {
-      if ( _state >= DefaultStates.Verification ) {
+    if (_state >= DefaultStates.Verification) {
       _appExitReason = result match {
         case Success => ApplicationExitReason.VERIFICATION_SUCCEEDED
         case Failure(_) => ApplicationExitReason.VERIFICATION_FAILED
@@ -55,7 +56,10 @@ trait SilFrontend extends DefaultFrontend {
   def resetPlugins(): Unit = {
     val pluginsArg: Option[String] = if (_config != null) {
       // concat defined plugins and default plugins
-      val list = _config.plugin.toOption ++ (if (_config.disableDefaultPlugins()) Seq() else defaultPlugins)
+      val list = (if (_config.enableSmokeDetection()) Set(smokeDetectionPlugin, refutePlugin) else Set()) ++
+        (if (_config.disableDefaultPlugins()) Set() else defaultPlugins) ++
+        _config.plugin.toOption.toSet
+
       if (list.isEmpty) {
         None
       } else {
@@ -75,12 +79,13 @@ trait SilFrontend extends DefaultFrontend {
   def createVerifier(fullCmd: String): Verifier
 
   /** Configures the verifier by passing it the command line arguments ''args''.
-    * Returns the verifier's effective configuration.
-    */
+   * Returns the verifier's effective configuration.
+   */
   def configureVerifier(args: Seq[String]): SilFrontendConfig
 
   /** The Viper verifier to be used for verification (after it has been initialized). */
   def verifier: Verifier = _ver
+
   protected var _ver: Verifier = _
 
   override protected type ParsingResult = PProgram
@@ -88,8 +93,12 @@ trait SilFrontend extends DefaultFrontend {
 
   /** The current configuration. */
   protected var _config: SilFrontendConfig = _
+
   def config: SilFrontendConfig = _config
 
+  private val refutePlugin: String = "viper.silver.plugin.standard.refute.RefutePlugin"
+  private val smokeDetectionPlugin: String = "viper.silver.plugin.standard.smoke.SmokeDetectionPlugin"
+
   /**
    * Default plugins are always activated and are run as last plugins.
    * All default plugins can be excluded from the plugins by providing the --disableDefaultPlugins flag
@@ -97,9 +106,10 @@ trait SilFrontend extends DefaultFrontend {
   private val defaultPlugins: Seq[String] = Seq(
     "viper.silver.plugin.standard.adt.AdtPlugin",
     "viper.silver.plugin.standard.termination.TerminationPlugin",
-    "viper.silver.plugin.standard.refute.RefutePlugin",
-    "viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin"
+    "viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin",
+    refutePlugin
   )
+
   /** For testing of plugin import feature */
   def defaultPluginCount: Int = defaultPlugins.size
 
@@ -116,6 +126,7 @@ trait SilFrontend extends DefaultFrontend {
   def plugins: SilverPluginManager = _plugins
 
   protected var _startTime: Long = _
+
   def startTime: Time = _startTime
 
   def getTime: Long = System.currentTimeMillis() - _startTime
@@ -124,13 +135,13 @@ trait SilFrontend extends DefaultFrontend {
     Consistency.resetMessages()
   }
 
-  def setVerifier(verifier:Verifier): Unit = {
+  def setVerifier(verifier: Verifier): Unit = {
     _ver = verifier
   }
 
   def prepare(args: Seq[String]): Boolean = {
 
-    reporter report CopyrightReport(_ver.signature)//${_ver.copyright}") // we agreed on 11/03/19 to drop the copyright
+    reporter report CopyrightReport(_ver.signature) //${_ver.copyright}") // we agreed on 11/03/19 to drop the copyright
 
     /* Parse command line arguments and populate _config */
     parseCommandLine(args)
@@ -189,16 +200,16 @@ trait SilFrontend extends DefaultFrontend {
       finish()
     }
     catch {
-        case MissingDependencyException(msg) =>
-          println("Missing dependency exception: " + msg)
-          reporter report MissingDependencyReport(msg)
+      case MissingDependencyException(msg) =>
+        println("Missing dependency exception: " + msg)
+        reporter report MissingDependencyReport(msg)
     }
   }
 
   override def reset(input: Path): Unit = {
     super.reset(input)
 
-    if(_config != null) {
+    if (_config != null) {
       resetPlugins()
     }
   }
@@ -224,7 +235,7 @@ trait SilFrontend extends DefaultFrontend {
   }
 
   override def verification(): Unit = {
-    def filter(input: Program): Result[Program]  = {
+    def filter(input: Program): Result[Program] = {
       plugins.beforeMethodFilter(input) match {
         case Some(inputPlugin) =>
           // Filter methods according to command-line arguments.
@@ -277,7 +288,10 @@ trait SilFrontend extends DefaultFrontend {
         val result = fp.parse(inputPlugin, file, Some(plugins))
         if (result.errors.forall(p => p.isInstanceOf[ParseWarning])) {
           reporter report WarningsDuringParsing(result.errors)
-          Succ({result.initProperties(); result})
+          Succ({
+            result.initProperties();
+            result
+          })
         }
         else Fail(result.errors)
       case None => Fail(plugins.errors)
@@ -326,7 +340,7 @@ trait SilFrontend extends DefaultFrontend {
     }
   }
 
-  def doConsistencyCheck(input: Program): Result[Program]= {
+  def doConsistencyCheck(input: Program): Result[Program] = {
     var errors = input.checkTransitively
     if (backendTypeFormat.isDefined)
       errors = errors ++ Consistency.checkBackendTypes(input, backendTypeFormat.get)

From 3f0198a42cf3fe747e9bcc7be3722117dc086545 Mon Sep 17 00:00:00 2001
From: Lea Salome Brugger <leasalome.brugger@inf.ethz.ch>
Date: Mon, 8 Jan 2024 15:42:39 +0100
Subject: [PATCH 60/61] Add tests for smoke detection plugin

---
 src/test/resources/smoke/axiom.vpr            | 10 +++++++
 src/test/resources/smoke/if.vpr               | 19 +++++++++++++
 .../resources/smoke/infinite_loop-goto.vpr    |  6 +++++
 .../resources/smoke/infinite_loop-while.vpr   |  7 +++++
 src/test/resources/smoke/inhale-1.vpr         |  5 ++++
 src/test/resources/smoke/inhale-2.vpr         |  8 ++++++
 src/test/resources/smoke/inhale-3.vpr         |  9 +++++++
 src/test/resources/smoke/loop.vpr             | 14 ++++++++++
 src/test/resources/smoke/method-abstract.vpr  |  2 ++
 src/test/resources/smoke/method.vpr           |  5 ++++
 src/test/resources/smoke/unreachable-1.vpr    |  5 ++++
 src/test/resources/smoke/unreachable-2.vpr    | 27 +++++++++++++++++++
 src/test/resources/smoke/unreachable-3.vpr    | 25 +++++++++++++++++
 13 files changed, 142 insertions(+)
 create mode 100644 src/test/resources/smoke/axiom.vpr
 create mode 100644 src/test/resources/smoke/if.vpr
 create mode 100644 src/test/resources/smoke/infinite_loop-goto.vpr
 create mode 100644 src/test/resources/smoke/infinite_loop-while.vpr
 create mode 100644 src/test/resources/smoke/inhale-1.vpr
 create mode 100644 src/test/resources/smoke/inhale-2.vpr
 create mode 100644 src/test/resources/smoke/inhale-3.vpr
 create mode 100644 src/test/resources/smoke/loop.vpr
 create mode 100644 src/test/resources/smoke/method-abstract.vpr
 create mode 100644 src/test/resources/smoke/method.vpr
 create mode 100644 src/test/resources/smoke/unreachable-1.vpr
 create mode 100644 src/test/resources/smoke/unreachable-2.vpr
 create mode 100644 src/test/resources/smoke/unreachable-3.vpr

diff --git a/src/test/resources/smoke/axiom.vpr b/src/test/resources/smoke/axiom.vpr
new file mode 100644
index 000000000..f64540a88
--- /dev/null
+++ b/src/test/resources/smoke/axiom.vpr
@@ -0,0 +1,10 @@
+domain Foo {
+  axiom unsound {
+    false
+  }
+}
+
+//:: ExpectedOutput(refute.failed:refutation.true)
+method test()
+{
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/if.vpr b/src/test/resources/smoke/if.vpr
new file mode 100644
index 000000000..6100607e5
--- /dev/null
+++ b/src/test/resources/smoke/if.vpr
@@ -0,0 +1,19 @@
+//:: ExpectedOutput(refute.failed:refutation.true)
+method x()
+    ensures false
+{
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    assume 0 == 1
+}
+
+method test()
+{
+    var b: Bool
+
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    if (b) {
+        x()
+    } else {
+        
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/infinite_loop-goto.vpr b/src/test/resources/smoke/infinite_loop-goto.vpr
new file mode 100644
index 000000000..0d65bbed1
--- /dev/null
+++ b/src/test/resources/smoke/infinite_loop-goto.vpr
@@ -0,0 +1,6 @@
+//:: ExpectedOutput(refute.failed:refutation.true)
+method test()
+{
+    label l0
+    goto l0
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/infinite_loop-while.vpr b/src/test/resources/smoke/infinite_loop-while.vpr
new file mode 100644
index 000000000..8ad276ebb
--- /dev/null
+++ b/src/test/resources/smoke/infinite_loop-while.vpr
@@ -0,0 +1,7 @@
+//:: ExpectedOutput(refute.failed:refutation.true)
+method test()
+{
+    while (true)
+    {
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/inhale-1.vpr b/src/test/resources/smoke/inhale-1.vpr
new file mode 100644
index 000000000..c13c46221
--- /dev/null
+++ b/src/test/resources/smoke/inhale-1.vpr
@@ -0,0 +1,5 @@
+//:: ExpectedOutput(refute.failed:refutation.true)
+method test() {
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    assume false
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/inhale-2.vpr b/src/test/resources/smoke/inhale-2.vpr
new file mode 100644
index 000000000..8693bab84
--- /dev/null
+++ b/src/test/resources/smoke/inhale-2.vpr
@@ -0,0 +1,8 @@
+//:: ExpectedOutput(refute.failed:refutation.true)
+method test() returns (res: Int)
+    ensures res == 1
+{
+    res := 2
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    assume res == 1
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/inhale-3.vpr b/src/test/resources/smoke/inhale-3.vpr
new file mode 100644
index 000000000..4768933d5
--- /dev/null
+++ b/src/test/resources/smoke/inhale-3.vpr
@@ -0,0 +1,9 @@
+field x: Int
+
+//:: ExpectedOutput(refute.failed:refutation.true)
+method test(a: Ref)
+{
+    inhale acc(a.x)
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    inhale acc(a.x)
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/loop.vpr b/src/test/resources/smoke/loop.vpr
new file mode 100644
index 000000000..c146a4a19
--- /dev/null
+++ b/src/test/resources/smoke/loop.vpr
@@ -0,0 +1,14 @@
+function foo(): Bool
+{
+    false
+}
+
+method test(a: Bool)
+{
+
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    while (a) {
+        //:: ExpectedOutput(refute.failed:refutation.true)
+        assume foo()
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/method-abstract.vpr b/src/test/resources/smoke/method-abstract.vpr
new file mode 100644
index 000000000..fd7e53272
--- /dev/null
+++ b/src/test/resources/smoke/method-abstract.vpr
@@ -0,0 +1,2 @@
+method abstract()
+    requires false
\ No newline at end of file
diff --git a/src/test/resources/smoke/method.vpr b/src/test/resources/smoke/method.vpr
new file mode 100644
index 000000000..aabe0f71d
--- /dev/null
+++ b/src/test/resources/smoke/method.vpr
@@ -0,0 +1,5 @@
+//:: ExpectedOutput(refute.failed:refutation.true)
+method test()
+    requires false
+{
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/unreachable-1.vpr b/src/test/resources/smoke/unreachable-1.vpr
new file mode 100644
index 000000000..0929248d3
--- /dev/null
+++ b/src/test/resources/smoke/unreachable-1.vpr
@@ -0,0 +1,5 @@
+method test()
+    requires false
+{
+    unreachable
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/unreachable-2.vpr b/src/test/resources/smoke/unreachable-2.vpr
new file mode 100644
index 000000000..38d530909
--- /dev/null
+++ b/src/test/resources/smoke/unreachable-2.vpr
@@ -0,0 +1,27 @@
+method test7(a: Bool)
+    requires !a
+{
+
+    if (a) {
+        unreachable
+        assume false
+    }
+
+    if (a) {
+        unreachable
+        while (a) {
+            assume false
+
+            if (a) {
+                assume false
+            }
+        }
+    }
+
+    while (a) {
+        unreachable
+        if (a) {
+            assume false
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/smoke/unreachable-3.vpr b/src/test/resources/smoke/unreachable-3.vpr
new file mode 100644
index 000000000..48b116f78
--- /dev/null
+++ b/src/test/resources/smoke/unreachable-3.vpr
@@ -0,0 +1,25 @@
+method test(a: Bool)
+    requires !a
+{
+    if (a) {
+        unreachable
+    }
+    
+
+    var x: Int := 1
+
+    if (a) {
+        //:: ExpectedOutput(refute.failed:refutation.true)
+        assume false
+        unreachable
+        x := 0
+
+        if (x == 1) {
+            assume false
+
+            if (x == 1) {
+                assume false
+            }
+        }
+    }
+}
\ No newline at end of file

From 17b2b054d66198f009b3e6adfee1e766f7598cc6 Mon Sep 17 00:00:00 2001
From: Lea Salome Brugger <leasalome.brugger@inf.ethz.ch>
Date: Mon, 8 Jan 2024 16:48:01 +0100
Subject: [PATCH 61/61] Fix test for smoke detection such that it works with
 Silicon

---
 src/test/resources/smoke/axiom.vpr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/test/resources/smoke/axiom.vpr b/src/test/resources/smoke/axiom.vpr
index f64540a88..b991a947f 100644
--- a/src/test/resources/smoke/axiom.vpr
+++ b/src/test/resources/smoke/axiom.vpr
@@ -7,4 +7,5 @@ domain Foo {
 //:: ExpectedOutput(refute.failed:refutation.true)
 method test()
 {
+    var x: Foo
 }
\ No newline at end of file