diff options
| author | Alasdair Armstrong | 2019-04-15 14:15:09 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-15 17:22:55 +0100 |
| commit | fb88a51fbfd74482a4e5bcbada7c4c749db4d5ba (patch) | |
| tree | 6908de3f59734247d7ffe946f6ab6247b001f650 /src/sail.ml | |
| parent | 7cfbabc2bfba4f7d2ba0d3f91c7068ac3b1a84d1 (diff) | |
SMT: Allow partial specializations
Change specialisation so we only specialize integer parameters when
they are constant. This makes ensures that the integer-specialised
code is always type-correct.
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sail.ml b/src/sail.ml index 7d9d9d3b..575ffbdf 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -423,7 +423,7 @@ let target name out_name ast type_envs = let props = Property.find_properties ast in Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls; let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in - (* let ast_smt, type_envs = Specialize.(specialize' 1 int_specialization_with_externs ast_smt type_envs) in *) + let ast_smt, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_smt type_envs) in let name_file = match !opt_file_out with | Some f -> fun str -> f ^ "_" ^ str ^ ".smt2" |