From 8047e8af459e26f3a70d545f3d7f07de105c785b Mon Sep 17 00:00:00 2001
From: gauravpartha <49554253+gauravpartha@users.noreply.github.com>
Date: Sat, 21 Dec 2024 13:02:40 +0100
Subject: [PATCH] Update README.md

---
 README.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index cf56b4c6..600d065b 100644
--- a/README.md
+++ b/README.md
@@ -38,6 +38,8 @@ Our certificate shows for each procedure that the CFG right before the CFG-to-DA
 phase is correct under the assumption of the VC. That is, we support all the 
 transformation listed above except those listed in points 1 and 2.
 
+**Note: points 1 and 2 are also handled on [a separate branch](https://github.com/viperproject/boogie-proofgen/tree/cfg_optimizations) that has not yet been merged into this default branch.**
+
 ## Modifications to the VC
 We change the VC that Boogie generates in the following ways:
 1. We do not generate any axioms about built-in types that we do not support.
@@ -114,4 +116,4 @@ implies correctness of the input CFG of the CFG-to-DAG phase.
 When using the tool, one currently needs to make sure that no special characters
 are used that are reserved in Isabelle (such as `#` or `'`). Moreover, for
 files that do not verify, the tool cannot provide detailed information, since
-the counterexample information is not available.
\ No newline at end of file
+the counterexample information is not available.