if_decision_branch_Z3,4.6.0_WP.oracle 614 Bytes
Newer Older
1
Weakest Precondition
2
bench/ce/if_decision_branch.mlw Other VC f: Valid
3
bench/ce/if_decision_branch.mlw Other VC f: Unknown (sat)
4 5 6
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
7
"val" : "0" }
8
File if_decision_branch.mlw:
9 10 11
Line 18:
a, [] = {"type" : "Integer" ,
"val" : "0" }
12
Line 19:
13 14
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "22" }
15
Line 22:
16 17
TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@branch_id=5454]] = {"type" : "Boolean" ,
18
"val" : false }
19 20 21
Line 27:
TEMP_NAME, [[@introduced], [@model_trace:TEMP_NAME],
[@branch_id=121]] = {"type" : "Boolean" ,
22 23
"val" : false }