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/",