algebraic_types_mono_Z3,4.6.0_SP.oracle 2.27 KB
Newer Older
1
Strongest Postcondition
MARCHE Claude's avatar
MARCHE Claude committed
2
bench/ce/algebraic_types_mono.mlw M G: Unknown (sat)
3 4 5 6 7
Counter-example model:File algebraic_types_mono.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }

MARCHE Claude's avatar
MARCHE Claude committed
8
bench/ce/algebraic_types_mono.mlw M g2: Unknown (sat)
9 10 11 12 13 14
Counter-example model:File algebraic_types_mono.mlw:
Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }

MARCHE Claude's avatar
MARCHE Claude committed
15
bench/ce/algebraic_types_mono.mlw M g4: Unknown (sat)
16 17 18 19 20
Counter-example model:File algebraic_types_mono.mlw:
Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } }

MARCHE Claude's avatar
MARCHE Claude committed
21
bench/ce/algebraic_types_mono.mlw M g5: Unknown (sat)
22 23 24 25 26 27
Counter-example model:File algebraic_types_mono.mlw:
Line 16:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "1" }, {"type" : "Integer" ,
"val" : "0" }] } }

MARCHE Claude's avatar
MARCHE Claude committed
28
bench/ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
29 30 31 32 33 34 35 36 37 38 39 40 41
Counter-example model:File algebraic_types_mono.mlw:
Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "17" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "164" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "162" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "160" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "158" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }

MARCHE Claude's avatar
MARCHE Claude committed
42
bench/ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
43 44 45 46 47 48 49 50 51 52 53 54 55
Counter-example model:File algebraic_types_mono.mlw:
Line 27:
l, [[@introduced]] = {"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" : [] } }] } }] } }] } }] } }] } }