Merge pull request #114 from mtzguido/fix

EverParse3d.InputStream.Extern.fst: fix proof regression
project-everest · Nov 28, 2023 · b6680cf · b6680cf
2 parents 1daf54a + 1244967
commit b6680cf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/3d/prelude/extern/EverParse3d.InputStream.Extern.fst b/src/3d/prelude/extern/EverParse3d.InputStream.Extern.fst
@@ -219,7 +219,7 @@ let read
 
 #pop-options
 
-#push-options "--z3rlimit 64 --fuel 0 --ifuel 1 --z3cliopt smt.arith.nl=false --using_facts_from '* -FStar.Tactics -FStar.Reflection' --split_queries no"
+#push-options "--z3rlimit 32 --fuel 0 --ifuel 1 --z3cliopt smt.arith.nl=false --using_facts_from '* -FStar.Tactics -FStar.Reflection' --split_queries always --z3refresh"
 #restart-solver
 inline_for_extraction
 noextract