Increase rlimit.

cryspen · Jan 20, 2025 · 6cb5181 · 6cb5181
1 parent 33e910e
commit 6cb5181
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/examples/kyber_compress/proofs/fstar/extraction/Makefile b/examples/kyber_compress/proofs/fstar/extraction/Makefile
@@ -53,7 +53,7 @@ all:
 	rm -f .depend && $(MAKE) .depend
 	$(MAKE) verify
 
-HAX_CLI = "cargo hax into fstar --z3rlimit 200"
+HAX_CLI = "cargo hax into fstar --z3rlimit 500"
 
 # 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)