From 7dce6eaffaa4169fab822d833e32b593ad867588 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 May 2022 15:53:52 +0200
Subject: Update the extraction to set the fuel to 1 in the Z3 options

---
 src/Translate.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/Translate.ml b/src/Translate.ml
index 857f0f69..740670f9 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -573,8 +573,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
   (* Add the custom includes *)
   List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
-  (* Z3 options *)
-  Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 0 --ifuel 1\"\n";
+  (* Z3 options - note that we use fuel 1 because it its useful for the decrease clauses *)
+  Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 1 --ifuel 1\"\n";
 
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
-- 
cgit v1.2.3