Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [] = {"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]] = {"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]] = {"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]] = {"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]] = {"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]] = {"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
Counter-example model:File algebraic_type.mlw:
Line 8:
A, [] = {"proj_name" : "B_proj_1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }