algebraic_type_Z3,4.6.0.oracle 4.84 KB
Newer Older
Sylvain Dailler's avatar
Sylvain Dailler committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Weakest Precondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }

bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }

bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Sylvain Dailler's avatar
Sylvain Dailler committed
17 18 19 20 21 22
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }

Sylvain Dailler's avatar
Sylvain Dailler committed
23 24 25 26 27 28 29 30 31
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" },
{"type" : "Integer" ,
"val" : "0" }] } }

bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
32 33 34 35 36
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
37 38
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
39 40
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
Sylvain Dailler's avatar
Sylvain Dailler committed
41 42 43 44
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }

Sylvain Dailler's avatar
Sylvain Dailler committed
45
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
46 47 48 49 50 51 52 53 54 55 56 57 58
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }

59
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
60
Strongest Postcondition
61
bench/ce/algebraic_type.mlw M G: Unknown (sat)
62 63
Counter-example model:File algebraic_type.mlw:
Line 6:
64
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
65
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
66 67
"val" : "0" }] } }

68 69 70 71 72 73 74 75
bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }

bench/ce/algebraic_type.mlw M g4: Unknown (sat)
Sylvain Dailler's avatar
Sylvain Dailler committed
76 77 78 79 80 81
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }

82 83 84 85 86 87 88 89 90
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" },
{"type" : "Integer" ,
"val" : "0" }] } }

bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
91 92 93 94 95
Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
96 97
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
Sylvain Dailler's avatar
Sylvain Dailler committed
98
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
99 100
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
Sylvain Dailler's avatar
Sylvain Dailler committed
101 102 103
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }

104
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
105 106 107 108 109 110 111 112 113 114 115 116 117
Counter-example model:File algebraic_type.mlw:
Line 27:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "21" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "10" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "9" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "7" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "8" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }

118
bench/ce/algebraic_type.mlw M g: Timeout or Unknown