From 48ae8dc7e98cb2851c87d0299373e1e5ca627eb7 Mon Sep 17 00:00:00 2001
From: Pieter Bos <p.h.bos@utwente.nl>
Date: Thu, 12 Oct 2023 09:00:11 +0200
Subject: [PATCH] fix #1061: propagate c_e to framedproof

---
 src/rewrite/vct/rewrite/PropagateContextEverywhere.scala | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala b/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala
index 4883352c3f..00221ca661 100644
--- a/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala
+++ b/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala
@@ -94,6 +94,9 @@ case class PropagateContextEverywhere[Pre <: Generation]() extends Rewriter[Pre]
           loop.rewrite(contract = LoopInvariant(freshInvariants() &* dispatch(invariant), decreases.map(dispatch))(inv.blame))
         case _: IterationContract[Pre] => throw ExtraNode
       }
+    case frame: FramedProof[Pre] =>
+      implicit val o: Origin = frame.o
+      frame.rewrite(pre = freshInvariants() &* dispatch(frame.pre), post = freshInvariants() &* dispatch(frame.post))
     case other => rewriteDefault(other)
   }