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
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)