diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Translate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 *) |