From 5121432d179dfd6a6ca5c51912c9041e3cb50f21 Mon Sep 17 00:00:00 2001
From: alexanderjsummers <alex.summers@ubc.ca>
Date: Mon, 3 Jul 2023 18:11:49 -0700
Subject: [PATCH 1/2] try out A ==> B to A ==> A && B conversion

---
 src/main/scala/viper/carbon/boogie/Optimizer.scala | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/main/scala/viper/carbon/boogie/Optimizer.scala b/src/main/scala/viper/carbon/boogie/Optimizer.scala
index 6f84c243..86acccf8 100644
--- a/src/main/scala/viper/carbon/boogie/Optimizer.scala
+++ b/src/main/scala/viper/carbon/boogie/Optimizer.scala
@@ -17,6 +17,7 @@ object Optimizer {
    * - Constant folding for booleans, integers and reals.
    * - Removal of dead branches.
    * - Removal of assertions known to hold.
+   * - Experimental: all *remaining* A ==> B expressions / assertions become A ==> A && B
    *
    * Constant folding partly taken from  Transformer.simplify from SIL, but added more optimizations.
    */
@@ -42,6 +43,9 @@ object Optimizer {
       case BinExp(TrueLit(), Implies, FalseLit()) => FalseLit()
       case BinExp(TrueLit(), Implies, consequent) => consequent
 
+      // experiment: make all A ==> B into A ==> A && B
+      case BinExp(left, Implies, right) => BinExp(left, Implies, BinExp(left, And, right))
+
       case BinExp(BoolLit(left), EqCmp, BoolLit(right)) => BoolLit(left == right)
       case BinExp(FalseLit(), EqCmp, right) => UnExp(Not, right)
       case BinExp(left, EqCmp, FalseLit()) => UnExp(Not, left)

From 9ec2b83eaaf614de210c54e7e168013e5165ebab Mon Sep 17 00:00:00 2001
From: alexanderjsummers <alex.summers@ubc.ca>
Date: Tue, 25 Jun 2024 11:56:19 -0700
Subject: [PATCH 2/2] Update .gitignore

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 285bd97f..08a0e6c0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,3 +16,4 @@ tmp/
 results.txt
 *.bpl
 *.bpl.*
+z3.log