diff options
| author | Son Ho | 2022-05-06 15:53:52 +0200 |
|---|---|---|
| committer | Son Ho | 2022-05-06 15:53:52 +0200 |
| commit | 7dce6eaffaa4169fab822d833e32b593ad867588 (patch) | |
| tree | 08d3f6fe9fcf5e601affc8377a53bdd92c2a98f8 /src | |
| parent | 38276f00f6aaebb70392775b97577c73a657005a (diff) | |
Update the extraction to set the fuel to 1 in the Z3 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 *) |