int32_CVC4,1.5_WP.oracle 841 Bytes
Newer Older
1
Weakest Precondition
2 3
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
4
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
5 6
Counter-example model:File int32.mlw:
Line 6:
7 8
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
9
"val" : "22" } }
10
Line 8:
11
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
12
"value" : {"type" : "Integer" , "val" : "84" } }
13 14 15
r, [[@introduced],
[@model_trace:r]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
16
"val" : "84" } }
17
Line 9:
18 19
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
20
"val" : "42" } }
21 22 23 24
Line 10:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
25