From 3668e7226ef3c75a7dcb2faa6ce1d6fa90372a0d Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Thu, 5 Sep 2024 15:16:38 -0700
Subject: [PATCH] enable context pruning

---
 Pulse.fst.config.json                      | 4 +++-
 lib/pulse/core/Pulse.fst.config.json       | 4 +++-
 share/pulse/Makefile.include-base          | 2 +-
 share/pulse/examples/Pulse.fst.config.json | 4 +++-
 src/checker/PulseChecker.fst.config.json   | 4 +++-
 5 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/Pulse.fst.config.json b/Pulse.fst.config.json
index bdcf0bbd3..78ae24736 100644
--- a/Pulse.fst.config.json
+++ b/Pulse.fst.config.json
@@ -3,7 +3,9 @@
   "options": [
     "--query_cache",
     "--load_cmxs",
-    "pulse"
+    "pulse",
+    "--ext",
+    "context_pruning"
   ],
   "include_dirs": [
     "lib/pulse",
diff --git a/lib/pulse/core/Pulse.fst.config.json b/lib/pulse/core/Pulse.fst.config.json
index ab3f5d099..cf6a55f62 100644
--- a/lib/pulse/core/Pulse.fst.config.json
+++ b/lib/pulse/core/Pulse.fst.config.json
@@ -1,7 +1,9 @@
 {
 	"fstar_exe": "fstar.exe",
 	"options": [
-		"--query_cache"
+		"--query_cache",
+		"--ext",
+		"context_pruning"
 	],
 	"include_dirs": [
 	]
diff --git a/share/pulse/Makefile.include-base b/share/pulse/Makefile.include-base
index 66c72afe3..b147a9a11 100644
--- a/share/pulse/Makefile.include-base
+++ b/share/pulse/Makefile.include-base
@@ -19,7 +19,7 @@ else
 USE_HINTS:=
 endif
 
-FSTAR_OPTIONS += $(USE_HINTS)
+FSTAR_OPTIONS += $(USE_HINTS) --ext context_pruning
 
 # A place to put all build artifacts
 ifneq (,$(OUTPUT_DIRECTORY))
diff --git a/share/pulse/examples/Pulse.fst.config.json b/share/pulse/examples/Pulse.fst.config.json
index 935619e0b..51f3a0063 100644
--- a/share/pulse/examples/Pulse.fst.config.json
+++ b/share/pulse/examples/Pulse.fst.config.json
@@ -7,7 +7,9 @@
     "--cache_dir",
     "_output/cache",
     "--warn_error", 
-    "-249"
+    "-249",
+    "--ext",
+    "context_pruning"
   ],
   "include_dirs": [
     "../../../lib/pulse",
diff --git a/src/checker/PulseChecker.fst.config.json b/src/checker/PulseChecker.fst.config.json
index 57c55c95f..a4a4dc6a1 100644
--- a/src/checker/PulseChecker.fst.config.json
+++ b/src/checker/PulseChecker.fst.config.json
@@ -1,7 +1,9 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
-    "--query_cache"
+    "--query_cache",
+    "--ext",
+    "context_pruning"
   ],
   "include_dirs": [
   ]