algebraic_type_CVC4,1.5_SP.oracle 1.74 KB
Newer Older
1
Strongest Postcondition
2
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
3 4
Counter-example model:File algebraic_type.mlw:
Line 6:
5 6
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
7
"val" : "0" }] } }
8 9
x, [] = {"type" : "Integer" ,
"val" : "0" }
10

11 12 13
bench/ce/algebraic_type.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 10:
14 15
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" ,
16 17 18
"val" : "0" }] } }

bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
19 20
Counter-example model:File algebraic_type.mlw:
Line 12:
21
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
22 23
"list" : [] } }

24 25 26
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 16:
27 28
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" ,
29 30 31
"val" : "1" }] } }

bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
32 33
Counter-example model:File algebraic_type.mlw:
Line 25:
34 35 36
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "-1" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
37 38
"list" : [] } }] } }

39
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
40 41
Counter-example model:File algebraic_type.mlw:
Line 27:
42 43 44
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
45 46
"list" : [] } }] } }

47
bench/ce/algebraic_type.mlw M g: Timeout or Unknown
48 49 50 51 52 53
Counter-example model:File algebraic_type.mlw:
Line 8:
A, [] = {"proj_name" : "B_proj_1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }