Merge pull request #712 from viperproject/meilers_simplifier_equality

Disable simplification of equalities
viperproject · Jun 30, 2023 · 86d3ab9 · 86d3ab9
2 parents 0e92e92 + 11fc379
commit 86d3ab9
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -45,7 +45,9 @@ object Simplifier {
         FalseLit()(root.pos, root.info)
       case Implies(TrueLit(), consequent) => consequent
 
-      case root @ EqCmp(left, right) if left == right => TrueLit()(root.pos, root.info)
+      // ME: Disabled since it is not equivalent in case the expression is not well-defined.
+      // TODO: Consider checking if Expressions.proofObligations(left) is empty (requires adding the program as parameter).
+      // case root @ EqCmp(left, right) if left == right => TrueLit()(root.pos, root.info)
       case root @ EqCmp(BoolLit(left), BoolLit(right)) =>
         BoolLit(left == right)(root.pos, root.info)
       case root @ EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info)

diff --git a/src/test/scala/SimplifierTests.scala b/src/test/scala/SimplifierTests.scala
@@ -50,5 +50,11 @@ class SimplifierTests extends AnyFunSuite with Matchers {
     simplify(Mod(-3, -8)()) should be (5: IntLit)
   }
 
+  test("equality") {
+    val seqAcc = SeqIndex(EmptySeq(Int)(), 0: IntLit)()
+    // Do not simplify away definedness issues.
+    simplify(EqCmp(seqAcc, seqAcc)()) should be(EqCmp(seqAcc, seqAcc)())
+  }
+
   implicit def int2IntLit(i: Int): IntLit = IntLit(i)()
 }