Commit eef6d838 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make some examples pass with Jessie.

parent 95b2438a
...@@ -184,7 +184,7 @@ let uint32_module = ...@@ -184,7 +184,7 @@ let uint32_module =
let uint32_type : Why3.Ty.tysymbol = let uint32_type : Why3.Ty.tysymbol =
Mlw_module.ns_find_ts uint32_module.Mlw_module.mod_export ["t"] Mlw_module.ns_find_ts uint32_module.Mlw_module.mod_export ["t"]
let uint32_to_int : Term.lsymbol = find_ls uint32_module "to_uint" let uint32_to_int : Term.lsymbol = find_ls uint32_module "t'int"
let uadd32_fun : Mlw_expr.psymbol = find_ps uint32_module "add_check" let uadd32_fun : Mlw_expr.psymbol = find_ps uint32_module "add_check"
......
...@@ -70,11 +70,13 @@ let process () = ...@@ -70,11 +70,13 @@ let process () =
List.fold_left List.fold_left
(get_prover ACSLtoWhy3.config ACSLtoWhy3.env) (get_prover ACSLtoWhy3.config ACSLtoWhy3.env)
[] []
[ "Z432", "Z3,4.3.2,"; [ (*"Z432", "Z3,4.3.2,";
"Z440", "Z3,4.4.0,"; "Z440", "Z3,4.4.0,";
"C241", "CVC3,2.4.1,"; "C241", "CVC3,2.4.1,";
"C414", "CVC4,1.4,"; "C414", "CVC4,1.4,";
"A991", "Alt-Ergo,0.99.1,"; "A991", "Alt-Ergo,0.99.1,";*)
"Z460", "Z3,4.6.0,";
"A220", "Alt-Ergo,2.2.0,";
] ]
with e -> with e ->
ACSLtoWhy3.Self.fatal "Exception raised when loading prover drivers:@ %a" ACSLtoWhy3.Self.fatal "Exception raised when loading prover drivers:@ %a"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment