fix #1061: propagate c_e to framedproof

utwente-fmt · Oct 12, 2023 · 48ae8dc · 48ae8dc
1 parent bda21b5
commit 48ae8dc
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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)
   }