From f9208aba4f40d6eb9317c2b4da691c4bf918b202 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 13 Jul 2023 17:36:51 -0700 Subject: [PATCH] rlimit --- src/lowparse/LowParse.SteelST.List.Iter.WithInterrupt.fst | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/lowparse/LowParse.SteelST.List.Iter.WithInterrupt.fst b/src/lowparse/LowParse.SteelST.List.Iter.WithInterrupt.fst index 741edd6ab..53e92b770 100644 --- a/src/lowparse/LowParse.SteelST.List.Iter.WithInterrupt.fst +++ b/src/lowparse/LowParse.SteelST.List.Iter.WithInterrupt.fst @@ -101,6 +101,9 @@ let rec list_iter_with_interrupt_close_false list_iter_with_interrupt_close_false p state f_false _ bin cur' _ _ end +#pop-options + +#push-options "--z3rlimit 32" #restart-solver let list_iter_with_interrupt_close @@ -158,6 +161,9 @@ let list_iter_with_interrupt_close cont end +#pop-options + +#push-options "--z3rlimit 16" #restart-solver inline_for_extraction