Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 796ee891 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update CE bench after addition of soft time limit for Z3

parent b8340d4e
ce/array_records.mlw Array_records WP_parameter var_overwrite : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -15,38 +11,14 @@ ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records WP_parameter var_overwrite : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Timeout
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
......@@ -11,14 +11,14 @@ ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Timeout
ce/array_records.mlw Array_records WP_parameter var_overwrite : Timeout
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Timeout
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Timeout
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Timeout
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Timeout
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Timeout
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Timeout
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Timeout
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Timeout
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
......@@ -5,19 +5,19 @@ Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test2 : Timeout
ce/int_overflow.mlw ModelInt test2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow : Valid
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Valid
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Unknown (other)
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Unknown (other)
Counter-example model:File int_overflow.mlw:
......@@ -25,16 +25,16 @@ Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test2 : Timeout
ce/int_overflow.mlw ModelInt test2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow : Valid
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Valid
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Unknown (other)
......@@ -7,17 +7,17 @@ x = {"type" : "Integer" ,
ce/int_overflow.mlw ModelInt test2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow : Valid
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Valid
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Unknown (other)
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Unknown (other)
Counter-example model:File int_overflow.mlw:
......@@ -27,14 +27,14 @@ x = {"type" : "Integer" ,
ce/int_overflow.mlw ModelInt test2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow : Valid
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Valid
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Timeout
ce/jlamp0.mlw M WP_parameter p1 : Timeout
ce/jlamp0.mlw M WP_parameter p1 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p1 : Timeout
ce/jlamp0.mlw M WP_parameter p1 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter f : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter g : Valid
ce/jlamp_array.mlw Array WP_parameter g : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter g : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter h : Valid
ce/jlamp_array.mlw Array WP_parameter h : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter f : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter h : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : Valid
ce/jlamp_array.mlw Array WP_parameter f : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter g : Valid
ce/jlamp_array.mlw Array WP_parameter g : Valid
ce/jlamp_array.mlw Array WP_parameter g : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter g : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter h : Valid
ce/jlamp_array.mlw Array WP_parameter h : Valid
ce/jlamp_array.mlw Array WP_parameter h : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_array.mlw Array WP_parameter h : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : Timeout
ce/jlamp_array.mlw Array WP_parameter f : Timeout
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter g : Valid
ce/jlamp_array.mlw Array WP_parameter g : Timeout
ce/jlamp_array.mlw Array WP_parameter g : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter h : Valid
ce/jlamp_array.mlw Array WP_parameter h : Timeout
ce/jlamp_array.mlw Array WP_parameter f : Timeout
ce/jlamp_array.mlw Array WP_parameter h : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter f : Valid
ce/jlamp_array.mlw Array WP_parameter f : Timeout
ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter g : Valid
ce/jlamp_array.mlw Array WP_parameter g : Valid
ce/jlamp_array.mlw Array WP_parameter g : Timeout
ce/jlamp_array.mlw Array WP_parameter g : Unknown (other)
ce/jlamp_array.mlw Array WP_parameter h : Valid
ce/jlamp_array.mlw Array WP_parameter h : Valid
ce/jlamp_array.mlw Array WP_parameter h : Timeout
ce/jlamp_array.mlw Array WP_parameter h : Unknown (other)
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Valid
ce/jlamp_projections.mlw Abstract WP_parameter p3 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
ce/jlamp_projections.mlw Record WP_parameter p4 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Valid
ce/jlamp_projections.mlw Abstract WP_parameter p3 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
ce/jlamp_projections.mlw Record WP_parameter p4 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Valid
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Timeout
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
ce/jlamp_projections.mlw Record WP_parameter p4 : Timeout
ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Valid
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Timeout
ce/jlamp_projections.mlw Abstract WP_parameter p3 : Unknown (other)
ce/jlamp_projections.mlw Record WP_parameter p4 : Valid
ce/jlamp_projections.mlw Record WP_parameter p4 : Timeout
ce/jlamp_projections.mlw Record WP_parameter p4 : Unknown (other)
......@@ -7,31 +7,11 @@ t = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
ce/map.mlw M WP_parameter test_map : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter test_map_multidim1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter test_map_multidim2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter proj_map_test1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter proj_map_test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter test_map : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
ce/map.mlw ModelMap t1 : Unknown (other)
Counter-example model:File map.mlw:
Line 5:
......@@ -41,28 +21,8 @@ t = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
ce/map.mlw M WP_parameter test_map : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter test_map_multidim1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter test_map_multidim2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter proj_map_test1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter proj_map_test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter test_map : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
......@@ -7,11 +7,11 @@ t = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
ce/map.mlw M WP_parameter test_map : Timeout
ce/map.mlw M WP_parameter test_map_multidim1 : Timeout
ce/map.mlw M WP_parameter test_map_multidim2 : Timeout
ce/map.mlw M WP_parameter proj_map_test1 : Timeout
ce/map.mlw M WP_parameter proj_map_test2 : Timeout
ce/map.mlw M WP_parameter test_map : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
ce/map.mlw ModelMap t1 : Unknown (other)
Counter-example model:File map.mlw:
Line 5:
......@@ -21,8 +21,8 @@ t = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
ce/map.mlw M WP_parameter test_map : Timeout
ce/map.mlw M WP_parameter test_map_multidim1 : Timeout
ce/map.mlw M WP_parameter test_map_multidim2 : Timeout
ce/map.mlw M WP_parameter proj_map_test1 : Timeout
ce/map.mlw M WP_parameter proj_map_test2 : Timeout
ce/map.mlw M WP_parameter test_map : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
ce/real.mlw ModelReal test1 : Timeout
ce/real.mlw ModelReal test2 : Timeout
ce/real.mlw ModelReal test1 : Timeout
ce/real.mlw ModelReal test2 : Timeout
ce/real.mlw ModelReal test1 : Unknown (other)
ce/real.mlw ModelReal test2 : Unknown (other)
ce/real.mlw ModelReal test1 : Unknown (other)
ce/real.mlw ModelReal test2 : Unknown (other)
ce/records.mlw M WP_parameter record_match_eval_test1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test3 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test4 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter test_record_match_eval_test5 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test3 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test4 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter test_record_match_eval_test5 : HighFailure
Prover exit status: exited with status 1
Prover output: