Try context pruning for barrett.

cryspen · Dec 18, 2024 · 20cee83 · 20cee83
1 parent 6701b54
commit 20cee83
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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)