algebraic_type_CVC4,1.5_WP.oracle 1.65 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
Weakest Precondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
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: Timeout or Unknown
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: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 12:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "A" ,
"list" : [] } }

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

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

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

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