From 7cbf01d0eb36b3f5751a80e7ab75fa45a9f0b6cf Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Fri, 3 Jun 2022 11:22:47 +0200
Subject: [PATCH 1/6] Add refutation plugin

---
 src/main/scala/viper/silver/ast/Ast.scala     |  8 ++
 .../viper/silver/frontend/SilFrontend.scala   |  1 +
 .../standard/refute/RefuteASTExtension.scala  | 20 +++++
 .../plugin/standard/refute/RefuteErrors.scala | 29 +++++++
 .../standard/refute/RefutePASTExtension.scala | 22 ++++++
 .../plugin/standard/refute/RefutePlugin.scala | 78 +++++++++++++++++++
 .../silver/verifier/VerificationError.scala   |  4 +
 src/test/resources/refute/simple.vpr          | 18 +++++
 8 files changed, 180 insertions(+)
 create mode 100644 src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
 create mode 100644 src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
 create mode 100644 src/main/scala/viper/silver/plugin/standard/refute/RefutePASTExtension.scala
 create mode 100644 src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
 create mode 100644 src/test/resources/refute/simple.vpr

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index a31458020..611b5d596 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -397,6 +397,14 @@ case object Synthesized extends Info {
   lazy val isCached = false
 }
 
+/** An `Info` instance for labelling an AST node which is expected to fail verification.
+ * This is used by Silicon to avoid stopping verification.
+*/
+class ExpectFail extends Info {
+  lazy val comment = Nil
+  lazy val isCached = false
+}
+
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   lazy val comment = head.comment ++ tail.comment
diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index 4b46f8d33..29c2138ec 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala
@@ -83,6 +83,7 @@ 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"
   )
   /** For testing of plugin import feature */
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
new file mode 100644
index 000000000..98399480a
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
@@ -0,0 +1,20 @@
+// 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.refute
+
+import viper.silver.ast._
+import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, text, toParenDoc}
+import viper.silver.ast.pretty.PrettyPrintPrimitives
+
+/** An `ExpectFail` info that tells us that this assert is a refute. */
+case object RefuteInfo extends ExpectFail
+
+case class Refute(exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt {
+  override lazy val prettyPrint: PrettyPrintPrimitives#Cont = text("refute") <+> toParenDoc(exp)
+
+  override val extensionSubnodes: Seq[Node] = Seq(exp)
+}
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
new file mode 100644
index 000000000..07336c604
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
@@ -0,0 +1,29 @@
+// 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.refute
+
+import viper.silver.verifier._
+
+case class RefuteFailed(override val offendingNode: Refute,
+                                    override val reason: ErrorReason,
+                                    override val cached: Boolean = false) extends AbstractVerificationError {
+  override val id = "refute.failed"
+  override val text = s"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)
+
+  override def withReason(r: ErrorReason): RefuteFailed = RefuteFailed(offendingNode, r, cached)
+}
+
+case class RefutationTrue(offendingNode: reasons.ErrorNode) extends AbstractErrorReason {
+  override val id: String = "refutation.true"
+
+  override val readableMessage: String = s"Assertion $offendingNode definitely holds."
+
+  override def withNode(offendingNode: reasons.ErrorNode): ErrorMessage = RefutationTrue(offendingNode)
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePASTExtension.scala
new file mode 100644
index 000000000..9f3e27de9
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePASTExtension.scala
@@ -0,0 +1,22 @@
+// 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.refute
+
+import viper.silver.ast.{Position, Stmt}
+import viper.silver.parser.TypeHelper.Bool
+import viper.silver.parser._
+
+case class PRefute(e: PExp)(val pos: (Position, Position)) extends PExtender with PStmt {
+  override val getSubnodes: Seq[PNode] = Seq(e)
+
+  override def typecheck(t: TypeChecker, n: NameAnalyser):Option[Seq[String]] = {
+    t.check(e, Bool)
+    None
+  }
+
+  override def translateStmt(t: Translator): Stmt = Refute(t.exp(e))(t.liftPos(this))
+}
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
new file mode 100644
index 000000000..3c2b96532
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -0,0 +1,78 @@
+// 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.refute
+
+import fastparse.P
+import viper.silver.ast.utility.ViperStrategy
+import viper.silver.ast._
+import viper.silver.parser.FastParser.{FP, exp, keyword, whitespace}
+import viper.silver.parser.ParserExtension
+import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
+import viper.silver.verifier._
+import viper.silver.verifier.errors.AssertFailed
+
+class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
+
+  /** Keyword used to define refute statements. */
+  private val RefuteKeyword: String = "refute"
+
+  private var RefuteAsserts: Map[Position, Refute] = Map()
+
+  /** Parser for refute statements. */
+  def refute[_: P]: P[PRefute] =
+    FP(keyword(RefuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
+
+  /** Add refute to the parser. */
+  override def beforeParse(input: String, isImported: Boolean): String = {
+    // Add new keyword
+    ParserExtension.addNewKeywords(Set[String](RefuteKeyword))
+    // Add new parser to the precondition
+    ParserExtension.addNewStmtAtEnd(refute(_))
+    input
+  }
+
+  /**
+   * Remove refute statements from the AST and add them as non-det asserts.
+   * The ⭐ is nice since such a variable name cannot be parsed, but will it cause issues?
+   */
+  override def beforeVerify(input: Program): Program = 
+    ViperStrategy.Slim({
+      case r@Refute(exp) => {
+        this.RefuteAsserts += (r.pos -> r)
+        Seqn(Seq(
+          If(LocalVar("⭐", Bool)(r.pos),
+            Seqn(Seq(
+              Assert(exp)(r.pos, RefuteInfo),
+              Inhale(BoolLit(false)(r.pos))(r.pos)
+            ), Seq())(r.pos),
+            Seqn(Seq(), Seq())(r.pos))(r.pos)
+          ),
+          Seq(LocalVarDecl("⭐", Bool)(r.pos))
+        )(r.pos)
+      }
+    }).recurseFunc({
+      case Method(_, _, _, _, _, body) => Seq(body)
+    }).execute(input)
+
+  /** Remove refutation related errors and add RefuteAsserts that didn't report an error. */
+  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
+    val errors: Seq[AbstractError] = (input match {
+      case Success => Seq()
+      case Failure(errors) => {
+        errors.filter {
+          case AssertFailed(a, _, _) if a.info == RefuteInfo => {
+            this.RefuteAsserts -= a.pos
+            false
+          }
+          case _ => true
+        }
+      }
+    }) ++ this.RefuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
+    if (errors.length == 0) Success
+    else Failure(errors)
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index ab4152630..817093c3e 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -153,6 +153,10 @@ trait ErrorMessage {
 
   // Should consider refactoring as a transformer, if/once we make the error message structure recursive
   def withNode(offendingNode: errors.ErrorNode = this.offendingNode) : ErrorMessage
+
+  // Check if the offendingNode contains any `ExpectFail` info tags
+  def isExpected: Boolean = if (!offendingNode.isInstanceOf[Infoed]) false
+    else offendingNode.asInstanceOf[Infoed].info.getUniqueInfo[ExpectFail].isDefined
 }
 
 trait VerificationError extends AbstractError with ErrorMessage {
diff --git a/src/test/resources/refute/simple.vpr b/src/test/resources/refute/simple.vpr
new file mode 100644
index 000000000..d7c0a9d5c
--- /dev/null
+++ b/src/test/resources/refute/simple.vpr
@@ -0,0 +1,18 @@
+method foo(x: Int) returns (r: Int)
+    requires x > 10
+{
+    refute !(x > 0)
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    refute x > 0
+    refute false
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    refute true
+    refute false
+    if (x > 0) {
+        r := x
+    } else {
+        //:: ExpectedOutput(refute.failed:refutation.true)
+        refute false
+        r := 0
+    }
+}
\ No newline at end of file

From ce219b746af2741492350b906dc426078b48f60e Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 13 Jun 2022 19:02:23 +0200
Subject: [PATCH 2/6] Some review changes

---
 src/main/scala/viper/silver/ast/Ast.scala     | 28 +++++++++----------
 .../standard/refute/RefuteASTExtension.scala  |  4 +--
 .../plugin/standard/refute/RefuteErrors.scala |  6 ++--
 .../plugin/standard/refute/RefutePlugin.scala |  2 +-
 .../silver/verifier/VerificationError.scala   |  4 +--
 5 files changed, 21 insertions(+), 23 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 611b5d596..f0b96609b 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -367,25 +367,25 @@ trait Info {
 
 /** A default `Info` that is empty. */
 case object NoInfo extends Info {
-  lazy val comment = Nil
-  lazy val isCached = false
+  override def comment = Nil
+  override def isCached = false
 }
 
 /** A simple `Info` that contains a list of comments. */
 case class SimpleInfo(comment: Seq[String]) extends Info {
-  lazy val isCached = false
+  override def isCached = false
 }
 
 /** An `Info` instance for labelling a quantifier as auto-triggered. */
 case object AutoTriggered extends Info {
-  lazy val comment = Nil
-  lazy val isCached = false
+  override def comment = Nil
+  override def isCached = false
 }
 
 /** An `Info` instance for labelling a pre-verified AST node (e.g., via caching). */
 case object Cached extends Info {
-  lazy val comment = Nil
-  lazy val isCached = true
+  override def comment = Nil
+  override def isCached = true
 }
 
 /** An `Info` instance for labelling a node as synthesized. A synthesized node is one that
@@ -393,22 +393,22 @@ case object Cached extends Info {
   * originate from an AST transformation.
   */
 case object Synthesized extends Info {
-  lazy val comment = Nil
-  lazy val isCached = false
+  override def comment = Nil
+  override def isCached = false
 }
 
 /** An `Info` instance for labelling an AST node which is expected to fail verification.
  * This is used by Silicon to avoid stopping verification.
 */
-class ExpectFail extends Info {
-  lazy val comment = Nil
-  lazy val isCached = false
+abstract class FailureExpectedInfo extends Info {
+  override def comment = Nil
+  override def isCached = false
 }
 
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
-  lazy val comment = head.comment ++ tail.comment
-  lazy val isCached = head.isCached || tail.isCached
+  override def comment = head.comment ++ tail.comment
+  override def isCached = head.isCached || tail.isCached
 }
 
 /** Build a `ConsInfo` instance out of two `Info`s, unless the latter is `NoInfo` (which can be dropped) */
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
index 98399480a..31e230819 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
@@ -10,8 +10,8 @@ import viper.silver.ast._
 import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, text, toParenDoc}
 import viper.silver.ast.pretty.PrettyPrintPrimitives
 
-/** An `ExpectFail` info that tells us that this assert is a refute. */
-case object RefuteInfo extends ExpectFail
+/** An `FailureExpectedInfo` info that tells us that this assert is a refute. */
+case object RefuteInfo extends FailureExpectedInfo
 
 case class Refute(exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt {
   override lazy val prettyPrint: PrettyPrintPrimitives#Cont = text("refute") <+> toParenDoc(exp)
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 07336c604..056b77358 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
@@ -8,11 +8,9 @@ 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 {
+case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
   override val id = "refute.failed"
-  override val text = s"Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)."
+  override val text = "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 3c2b96532..1ef7ef341 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -39,7 +39,7 @@ class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
    * Remove refute statements from the AST and add them as non-det asserts.
    * The ⭐ is nice since such a variable name cannot be parsed, but will it cause issues?
    */
-  override def beforeVerify(input: Program): Program = 
+  override def beforeVerify(input: Program): Program =
     ViperStrategy.Slim({
       case r@Refute(exp) => {
         this.RefuteAsserts += (r.pos -> r)
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 817093c3e..417f6f576 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -154,9 +154,9 @@ trait ErrorMessage {
   // Should consider refactoring as a transformer, if/once we make the error message structure recursive
   def withNode(offendingNode: errors.ErrorNode = this.offendingNode) : ErrorMessage
 
-  // Check if the offendingNode contains any `ExpectFail` info tags
+  // Check if the offendingNode contains any `FailureExpectedInfo` info tags
   def isExpected: Boolean = if (!offendingNode.isInstanceOf[Infoed]) false
-    else offendingNode.asInstanceOf[Infoed].info.getUniqueInfo[ExpectFail].isDefined
+    else offendingNode.asInstanceOf[Infoed].info.getUniqueInfo[FailureExpectedInfo].isDefined
 }
 
 trait VerificationError extends AbstractError with ErrorMessage {

From 44d270e09ebb16664194621f84a88b4a6d2a6331 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Mon, 13 Jun 2022 19:08:16 +0200
Subject: [PATCH 3/6] Make files end with newlines

---
 .../viper/silver/plugin/standard/refute/RefuteErrors.scala      | 2 +-
 .../viper/silver/plugin/standard/refute/RefutePlugin.scala      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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 056b77358..b75560bab 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala
@@ -24,4 +24,4 @@ case class RefutationTrue(offendingNode: reasons.ErrorNode) extends AbstractErro
   override val readableMessage: String = s"Assertion $offendingNode definitely holds."
 
   override def withNode(offendingNode: reasons.ErrorNode): ErrorMessage = RefutationTrue(offendingNode)
-}
\ No newline at end of file
+}
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 1ef7ef341..f3b246841 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -75,4 +75,4 @@ class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
     if (errors.length == 0) Success
     else Failure(errors)
   }
-}
\ No newline at end of file
+}

From 327c3d3e6ab24e9cc951407af3625addaa83e839 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Wed, 15 Jun 2022 18:05:37 +0200
Subject: [PATCH 4/6] Make pretty-printed program parseable

---
 .../viper/silver/plugin/standard/refute/RefutePlugin.scala    | 4 ++--
 src/test/resources/refute/simple.vpr                          | 2 +-
 2 files changed, 3 insertions(+), 3 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 f3b246841..a2eb55e8b 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -44,14 +44,14 @@ class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
       case r@Refute(exp) => {
         this.RefuteAsserts += (r.pos -> r)
         Seqn(Seq(
-          If(LocalVar("⭐", Bool)(r.pos),
+          If(LocalVar(s"__plugin_refute_nondet${this.RefuteAsserts.size}", Bool)(r.pos),
             Seqn(Seq(
               Assert(exp)(r.pos, RefuteInfo),
               Inhale(BoolLit(false)(r.pos))(r.pos)
             ), Seq())(r.pos),
             Seqn(Seq(), Seq())(r.pos))(r.pos)
           ),
-          Seq(LocalVarDecl("⭐", Bool)(r.pos))
+          Seq(LocalVarDecl(s"__plugin_refute_nondet${this.RefuteAsserts.size}", Bool)(r.pos))
         )(r.pos)
       }
     }).recurseFunc({
diff --git a/src/test/resources/refute/simple.vpr b/src/test/resources/refute/simple.vpr
index d7c0a9d5c..e7426f94f 100644
--- a/src/test/resources/refute/simple.vpr
+++ b/src/test/resources/refute/simple.vpr
@@ -15,4 +15,4 @@ method foo(x: Int) returns (r: Int)
         refute false
         r := 0
     }
-}
\ No newline at end of file
+}

From ee75d528631df7b94fe5c4ef919964bd548e8b0c Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Fri, 17 Jun 2022 13:09:04 +0100
Subject: [PATCH 5/6] Add test with branching

---
 src/test/resources/refute/complex.vpr | 36 +++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 src/test/resources/refute/complex.vpr

diff --git a/src/test/resources/refute/complex.vpr b/src/test/resources/refute/complex.vpr
new file mode 100644
index 000000000..d337042a1
--- /dev/null
+++ b/src/test/resources/refute/complex.vpr
@@ -0,0 +1,36 @@
+field f: Int
+
+function foo(x:Ref): Bool
+    requires acc(x.f) { x.f == x.f }
+
+method bar(y: Int)
+    requires y > 10
+{
+    var x: Ref
+    inhale acc(x.f)
+    label l
+    while (x.f > y)
+        invariant acc(x.f) && (old[l](x.f >= y) ==> x.f >= y)
+    {
+        refute x.f < y
+        x.f := x.f - 1
+        //:: ExpectedOutput(refute.failed:refutation.true)
+        refute foo(x)
+    }
+    refute x.f == y
+    
+    var z: Int
+    if (z > 10) {
+        z := z+1
+    } else {
+        z := z-1
+    }
+    if (z < -10) {
+        z := z+1
+    } else {
+        z := z-1
+    }
+    refute z == 10
+    //:: ExpectedOutput(refute.failed:refutation.true)
+    refute z < 9 || z > 10
+}

From 154c67d8b7edfa8523b871669b90e6fcb88f5285 Mon Sep 17 00:00:00 2001
From: Jonas <jonas.fiala.cardiff@gmail.com>
Date: Thu, 30 Jun 2022 16:26:33 +0200
Subject: [PATCH 6/6] Review changes

---
 src/main/scala/viper/silver/ast/Ast.scala     | 26 +++++++++----------
 .../plugin/standard/refute/RefutePlugin.scala | 20 +++++++-------
 .../termination/TerminationPlugin.scala       |  6 ++---
 .../silver/verifier/VerificationError.scala   |  6 +++--
 4 files changed, 30 insertions(+), 28 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index f0b96609b..0bbc75521 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -367,25 +367,25 @@ trait Info {
 
 /** A default `Info` that is empty. */
 case object NoInfo extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** A simple `Info` that contains a list of comments. */
 case class SimpleInfo(comment: Seq[String]) extends Info {
-  override def isCached = false
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling a quantifier as auto-triggered. */
 case object AutoTriggered extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling a pre-verified AST node (e.g., via caching). */
 case object Cached extends Info {
-  override def comment = Nil
-  override def isCached = true
+  override val comment = Nil
+  override val isCached = true
 }
 
 /** An `Info` instance for labelling a node as synthesized. A synthesized node is one that
@@ -393,22 +393,22 @@ case object Cached extends Info {
   * originate from an AST transformation.
   */
 case object Synthesized extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling an AST node which is expected to fail verification.
  * This is used by Silicon to avoid stopping verification.
 */
 abstract class FailureExpectedInfo extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
-  override def comment = head.comment ++ tail.comment
-  override def isCached = head.isCached || tail.isCached
+  override val comment = head.comment ++ tail.comment
+  override val isCached = head.isCached || tail.isCached
 }
 
 /** Build a `ConsInfo` instance out of two `Info`s, unless the latter is `NoInfo` (which can be dropped) */
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 a2eb55e8b..a9c9d5728 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -18,18 +18,18 @@ import viper.silver.verifier.errors.AssertFailed
 class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
 
   /** Keyword used to define refute statements. */
-  private val RefuteKeyword: String = "refute"
+  private val refuteKeyword: String = "refute"
 
-  private var RefuteAsserts: Map[Position, Refute] = Map()
+  private var refuteAsserts: Map[Position, Refute] = Map()
 
   /** Parser for refute statements. */
   def refute[_: P]: P[PRefute] =
-    FP(keyword(RefuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
+    FP(keyword(refuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
 
   /** Add refute to the parser. */
   override def beforeParse(input: String, isImported: Boolean): String = {
     // Add new keyword
-    ParserExtension.addNewKeywords(Set[String](RefuteKeyword))
+    ParserExtension.addNewKeywords(Set[String](refuteKeyword))
     // Add new parser to the precondition
     ParserExtension.addNewStmtAtEnd(refute(_))
     input
@@ -42,36 +42,36 @@ class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
   override def beforeVerify(input: Program): Program =
     ViperStrategy.Slim({
       case r@Refute(exp) => {
-        this.RefuteAsserts += (r.pos -> r)
+        this.refuteAsserts += (r.pos -> r)
         Seqn(Seq(
-          If(LocalVar(s"__plugin_refute_nondet${this.RefuteAsserts.size}", Bool)(r.pos),
+          If(LocalVar(s"__plugin_refute_nondet${this.refuteAsserts.size}", Bool)(r.pos),
             Seqn(Seq(
               Assert(exp)(r.pos, RefuteInfo),
               Inhale(BoolLit(false)(r.pos))(r.pos)
             ), Seq())(r.pos),
             Seqn(Seq(), Seq())(r.pos))(r.pos)
           ),
-          Seq(LocalVarDecl(s"__plugin_refute_nondet${this.RefuteAsserts.size}", Bool)(r.pos))
+          Seq(LocalVarDecl(s"__plugin_refute_nondet${this.refuteAsserts.size}", Bool)(r.pos))
         )(r.pos)
       }
     }).recurseFunc({
       case Method(_, _, _, _, _, body) => Seq(body)
     }).execute(input)
 
-  /** Remove refutation related errors and add RefuteAsserts that didn't report an error. */
+  /** Remove refutation related errors and add refuteAsserts that didn't report an error. */
   override def mapVerificationResult(input: VerificationResult): VerificationResult = {
     val errors: Seq[AbstractError] = (input match {
       case Success => Seq()
       case Failure(errors) => {
         errors.filter {
           case AssertFailed(a, _, _) if a.info == RefuteInfo => {
-            this.RefuteAsserts -= a.pos
+            this.refuteAsserts -= a.pos
             false
           }
           case _ => true
         }
       }
-    }) ++ this.RefuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
+    }) ++ this.refuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
     if (errors.length == 0) Success
     else Failure(errors)
   }
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 935a07092..af1c9a81e 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -28,7 +28,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
   /**
    * Keyword used to define decreases clauses
    */
-  private val DecreasesKeyword: String = "decreases"
+  private val decreasesKeyword: String = "decreases"
 
   /**
    * Parser for decreases clauses with following possibilities.
@@ -40,7 +40,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
    * decreases *
    */
   def decreases[_: P]: P[PDecreasesClause] =
-    P(keyword(DecreasesKeyword) ~/ (decreasesWildcard | decreasesStar | decreasesTuple) ~ ";".?)
+    P(keyword(decreasesKeyword) ~/ (decreasesWildcard | decreasesStar | decreasesTuple) ~ ";".?)
   def decreasesTuple[_: P]: P[PDecreasesTuple] =
     FP(exp.rep(sep = ",") ~/ condition.?).map { case (pos, (a, c)) => PDecreasesTuple(a, c)(pos) }
   def decreasesWildcard[_: P]: P[PDecreasesWildcard] = FP("_" ~/ condition.?).map{ case (pos, c) => PDecreasesWildcard(c)(pos) }
@@ -53,7 +53,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
    */
   override def beforeParse(input: String, isImported: Boolean): String = {
     // Add new keyword
-    ParserExtension.addNewKeywords(Set[String](DecreasesKeyword))
+    ParserExtension.addNewKeywords(Set[String](decreasesKeyword))
     // Add new parser to the precondition
     ParserExtension.addNewPreCondition(decreases(_))
     // Add new parser to the postcondition
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 417f6f576..af9464494 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -155,8 +155,10 @@ trait ErrorMessage {
   def withNode(offendingNode: errors.ErrorNode = this.offendingNode) : ErrorMessage
 
   // Check if the offendingNode contains any `FailureExpectedInfo` info tags
-  def isExpected: Boolean = if (!offendingNode.isInstanceOf[Infoed]) false
-    else offendingNode.asInstanceOf[Infoed].info.getUniqueInfo[FailureExpectedInfo].isDefined
+  def isExpected: Boolean = offendingNode match {
+    case i: Infoed => i.info.getUniqueInfo[FailureExpectedInfo].isDefined
+    case _ => false
+  }
 }
 
 trait VerificationError extends AbstractError with ErrorMessage {