From 20cee836d7cc996b44fc3c58000ff961f05cddc9 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Wed, 18 Dec 2024 09:14:02 +0100
Subject: [PATCH] Try context pruning for barrett.

---
 examples/barrett/proofs/fstar/extraction/Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/examples/barrett/proofs/fstar/extraction/Makefile b/examples/barrett/proofs/fstar/extraction/Makefile
index cbf5ee7af..dd213720a 100644
--- a/examples/barrett/proofs/fstar/extraction/Makefile
+++ b/examples/barrett/proofs/fstar/extraction/Makefile
@@ -53,7 +53,7 @@ all:
 	rm -f .depend && $(MAKE) .depend
 	$(MAKE) verify
 
-HAX_CLI = "cargo hax into fstar --z3rlimit 1500"
+HAX_CLI = "cargo hax into fstar --z3rlimit 1000"
 
 # If $HACL_HOME doesn't exist, clone it
 ${HACL_HOME}:
@@ -114,6 +114,7 @@ FSTAR_FLAGS = --cmi \
   --warn_error -331 \
   --cache_checked_modules --cache_dir $(CACHE_DIR) \
   --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
+   --ext context_pruning \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
 FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS)