if_assign_CVC4,1.5_SP.oracle 2.86 KB
Newer Older
1 2
Strongest Postcondition
bench/ce/if_assign.mlw Test VC f: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
3 4 5 6 7 8 9 10
Counter-example model:File if_assign.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 12:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }

11
bench/ce/if_assign.mlw Test VC f2: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
12 13 14 15 16 17 18 19
Counter-example model:File if_assign.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 18:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }

20
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 28
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
29
File if_assign.mlw:
30 31
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
32
Line 22:
33 34 35 36 37 38 39 40 41 42 43 44 45 46
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
47 48

bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
49 50 51
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
52
"val" : "-1" }
53 54 55 56
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
57
File if_assign.mlw:
58 59
Line 21:
a, [] = {"type" : "Integer" , "val" : "-1" }
60
Line 22:
61 62 63 64 65 66 67 68 69 70 71 72 73 74
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
75 76

bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
77 78 79
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
80
"val" : "0" }
81
File if_assign.mlw:
82 83 84
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "0" }
85
Line 34:
Sylvain Dailler's avatar
Sylvain Dailler committed
86 87
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
88 89 90

bench/ce/if_assign.mlw Test VC f4: Valid
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
91 92 93
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
94
"val" : "-1" }
95 96 97 98 99
File ref.mlw:
Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
100 101 102
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
103 104
Line 31:
the check fails with all inputs
105
Line 34:
Sylvain Dailler's avatar
Sylvain Dailler committed
106
x, [[@introduced]] = {"type" : "Integer" ,
107
"val" : "0" }
108 109 110
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
111