if_assign_CVC4,1.5_WP.oracle 2.07 KB
Newer Older
1 2 3 4 5 6 7
Weakest Precondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 12:
8
x, [[@introduced]] = {"type" : "Integer" ,
9 10 11 12 13 14 15 16
"val" : "42" }

bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 18:
17
x, [[@introduced]] = {"type" : "Integer" ,
18 19 20
"val" : "42" }

bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
21 22 23
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
24
"val" : "0" }
25 26 27
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
28
"val" : "42" }
29
File if_assign.mlw:
30 31
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
32
Line 22:
33 34
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
35 36 37
Line 25:
x, [] = {"type" : "Integer" ,
"val" : "42" }
38 39

bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
40 41 42
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
43
"val" : "-1" }
44 45 46
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
47
"val" : "18" }
48
File if_assign.mlw:
49 50
Line 21:
a, [] = {"type" : "Integer" , "val" : "-1" }
51
Line 22:
52 53
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
54 55 56
Line 27:
x, [] = {"type" : "Integer" ,
"val" : "18" }
57 58

bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
59 60 61
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
62
"val" : "0" }
63
File if_assign.mlw:
64 65 66
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "0" }
67
Line 34:
68
x, [[@introduced]] = {"type" : "Integer" ,
69 70 71 72 73
"val" : "42" }

bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
74 75 76
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
77
"val" : "-1" }
78 79 80 81 82
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
83 84 85
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
86 87
Line 31:
the check fails with all inputs
88 89 90
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
91