rlimit

Inria-Prosecco · Feb 12, 2024 · 0ab756f · 0ab756f
1 parent ff03d62
commit 0ab756f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib_list/ArrayListGen.fst b/lib_list/ArrayListGen.fst
@@ -3025,7 +3025,7 @@ val extend_insert_aux4 (#a: Type)
   )
 
 #restart-solver
-#push-options "--compat_pre_typed_indexed_effects --z3rlimit 400 --fuel 2 --ifuel 2 --split_queries always"
+#push-options "--compat_pre_typed_indexed_effects --z3rlimit 400 --fuel 2 --ifuel 2"
 let extend_insert_aux4 #a
   #pred1 #pred2 #pred3 #pred4 #pred5
   r n1 n2 k hd2 hd3 hd4 hd5 tl5 sz5 v1 gs0 i