Commit 60f277f6 authored by MARCHE Claude's avatar MARCHE Claude

CE example algebraic_types split in 2

parent 5eaa1d86
......@@ -33,11 +33,11 @@ is_xfail=false
decide_fail () {
case "$1" in
# Inconsistent results between two runs
"bench/ce/algebraic_type_Z3,4.6.0_SP")
is_xfail=true;;
# "bench/ce/algebraic_type_Z3,4.6.0_SP")
# is_xfail=true;;
# Inconsistent results between two runs
"bench/ce/algebraic_type_Z3,4.6.0_WP")
is_xfail=true;;
# "bench/ce/algebraic_type_Z3,4.6.0_WP")
# is_xfail=true;;
# Inconsistent results between two runs
"bench/ce/ref_mono_Z3,4.6.0_WP")
is_xfail=true;;
......
module M
use int.Int
type int_type = Integer int
goal G : forall x : int_type. match x with Integer y -> y > 0 end
type t = A | B int
goal g2: forall x. x = A
goal g4: forall x. x = B 0
type u = Au int int
goal g5: forall x. x = Au 0 0
type mylist = | Nil | Cons int mylist
let rec function len l = match l with
| Nil -> 0
| Cons _ l' -> 1 + len l'
end
goal g1: forall l: mylist. len l = 0
goal g7: forall l: mylist. l = Nil
end
Strongest Postcondition
ce/algebraic_types_mono.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
ce/algebraic_types_mono.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } }
ce/algebraic_types_mono.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 16:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" ,
"val" : "1" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "-1" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 27:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }
Weakest Precondition
ce/algebraic_types_mono.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
ce/algebraic_types_mono.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } }
ce/algebraic_types_mono.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 16:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" ,
"val" : "1" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "-1" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw:
Line 27:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }
Strongest Postcondition
ce/algebraic_types_mono.mlw M G: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
ce/algebraic_types_mono.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw:
Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw:
Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } }
ce/algebraic_types_mono.mlw M g5: Unknown (sat)
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" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
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" : [] } }] } }] } }] } }] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
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" : [] } }] } }] } }] } }] } }] } }
Weakest Precondition
ce/algebraic_types_mono.mlw M G: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
ce/algebraic_types_mono.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw:
Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw:
Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } }
ce/algebraic_types_mono.mlw M g5: Unknown (sat)
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" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
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" : [] } }] } }] } }] } }] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
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" : [] } }] } }] } }] } }] } }] } }
module M
use int.Int
type int_type = Integer int
goal G : forall x : int_type. match x with Integer y -> y > 0 end
type t = A | B int
goal g2: forall x. x = A
goal g4: forall x. x = B 0
type u = Au int int
goal g5: forall x. x = Au 0 0
type mylist = | Nil | Cons int mylist
let rec function len l = match l with
| Nil -> 0
| Cons _ l' -> 1 + len l'
end
goal g1: forall l: mylist. len l = 0
goal g7: forall l: mylist. l = Nil
use list.List
use list.Length
......
Strongest Postcondition
ce_xfail/algebraic_types_poly.mlw M g: Timeout or Unknown
Weakest Precondition
ce_xfail/algebraic_types_poly.mlw M g: Timeout or Unknown
Strongest Postcondition
ce_xfail/algebraic_types_poly.mlw M g: Timeout or Unknown
Weakest Precondition
ce_xfail/algebraic_types_poly.mlw M g: Timeout or Unknown
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment