From 8c81d8e8c6841e0496e6d4ebaea9bdb9055b219b Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Tue, 3 Sep 2024 12:23:46 -0700
Subject: [PATCH] set context pruning in .fst.config.json files for use in
 vscode

---
 FStar.fst.config.json                        | 3 ++-
 examples/miniparse/MiniParse.fst.config.json | 1 +
 tests/hacl/HaclTests.fst.config.json         | 2 ++
 tests/vale/ValeTest.fst.config.json          | 3 ++-
 4 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/FStar.fst.config.json b/FStar.fst.config.json
index 2fc361406e6..9e7e90ab41d 100644
--- a/FStar.fst.config.json
+++ b/FStar.fst.config.json
@@ -1,7 +1,8 @@
 {
   "fstar_exe": "./bin/fstar.exe",
   "options": [
-    "--cache_dir", ".cache"
+    "--cache_dir", ".cache",
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
     "ulib/",
diff --git a/examples/miniparse/MiniParse.fst.config.json b/examples/miniparse/MiniParse.fst.config.json
index 6d6e73162ba..af60a2e69e8 100644
--- a/examples/miniparse/MiniParse.fst.config.json
+++ b/examples/miniparse/MiniParse.fst.config.json
@@ -1,6 +1,7 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
   ]
diff --git a/tests/hacl/HaclTests.fst.config.json b/tests/hacl/HaclTests.fst.config.json
index 6d6e73162ba..81a0d9b5da4 100644
--- a/tests/hacl/HaclTests.fst.config.json
+++ b/tests/hacl/HaclTests.fst.config.json
@@ -1,6 +1,8 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
+    "--ext", "context_pruning",
+    "--z3limit_factor", "2"
   ],
   "include_dirs": [
   ]
diff --git a/tests/vale/ValeTest.fst.config.json b/tests/vale/ValeTest.fst.config.json
index b22de359915..fd4218b2d38 100644
--- a/tests/vale/ValeTest.fst.config.json
+++ b/tests/vale/ValeTest.fst.config.json
@@ -1,7 +1,8 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
-    "--cache_dir", ".cache"
+    "--cache_dir", ".cache",
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
     "../../ulib/",