Commit 7e6e9d03 authored by MARCHE Claude's avatar MARCHE Claude

CE bench: fix oracles

parent 60f277f6
Strongest Postcondition Strongest Postcondition
ce/algebraic_types_mono.mlw M G: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 6: Line 6:
x, [[@introduced]] = {"type" : "Integer" , x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" } "val" : "0" }
ce/algebraic_types_mono.mlw M g2: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 10: Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 12: Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
ce/algebraic_types_mono.mlw M g5: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 16: Line 16:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" , "list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" ,
"val" : "1" }] } } "val" : "1" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 25: Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
...@@ -33,7 +33,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , ...@@ -33,7 +33,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } } "list" : [] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 27: Line 27:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
......
Weakest Precondition Weakest Precondition
ce/algebraic_types_mono.mlw M G: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 6: Line 6:
x, [[@introduced]] = {"type" : "Integer" , x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" } "val" : "0" }
ce/algebraic_types_mono.mlw M g2: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 10: Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g4: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 12: Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
ce/algebraic_types_mono.mlw M g5: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 16: Line 16:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" , "list" : [{"type" : "Integer" , "val" : "0" }, {"type" : "Integer" ,
"val" : "1" }] } } "val" : "1" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 25: Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
...@@ -33,7 +33,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , ...@@ -33,7 +33,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } } "list" : [] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 27: Line 27:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
......
Strongest Postcondition Strongest Postcondition
ce/algebraic_types_mono.mlw M G: Unknown (sat) bench/ce/algebraic_types_mono.mlw M G: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 6: Line 6:
x, [[@introduced]] = {"type" : "Integer" , x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" } "val" : "0" }
ce/algebraic_types_mono.mlw M g2: Unknown (sat) bench/ce/algebraic_types_mono.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 10: Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Unknown (sat) bench/ce/algebraic_types_mono.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 12: Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
ce/algebraic_types_mono.mlw M g5: Unknown (sat) bench/ce/algebraic_types_mono.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 16: Line 16:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "1" }, {"type" : "Integer" , "list" : [{"type" : "Integer" , "val" : "1" }, {"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 25: Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
...@@ -39,7 +39,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , ...@@ -39,7 +39,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } } "list" : [] } }] } }] } }] } }] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 27: Line 27:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
......
Weakest Precondition Weakest Precondition
ce/algebraic_types_mono.mlw M G: Unknown (sat) bench/ce/algebraic_types_mono.mlw M G: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 6: Line 6:
x, [[@introduced]] = {"type" : "Integer" , x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" } "val" : "0" }
ce/algebraic_types_mono.mlw M g2: Unknown (sat) bench/ce/algebraic_types_mono.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 10: Line 10:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "B" ,
"list" : [{"type" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
ce/algebraic_types_mono.mlw M g4: Unknown (sat) bench/ce/algebraic_types_mono.mlw M g4: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 12: Line 12:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "A" ,
"list" : [] } } "list" : [] } }
ce/algebraic_types_mono.mlw M g5: Unknown (sat) bench/ce/algebraic_types_mono.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 16: Line 16:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" , x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Au" ,
"list" : [{"type" : "Integer" , "val" : "1" }, {"type" : "Integer" , "list" : [{"type" : "Integer" , "val" : "1" }, {"type" : "Integer" ,
"val" : "0" }] } } "val" : "0" }] } }
ce/algebraic_types_mono.mlw M g1: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g1: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 25: Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
...@@ -39,7 +39,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , ...@@ -39,7 +39,7 @@ l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"val" : {"apply" : "Nil" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } } "list" : [] } }] } }] } }] } }] } }] } }
ce/algebraic_types_mono.mlw M g7: Timeout or Unknown bench/ce/algebraic_types_mono.mlw M g7: Timeout or Unknown
Counter-example model:File algebraic_types_mono.mlw: Counter-example model:File algebraic_types_mono.mlw:
Line 27: Line 27:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" , l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
......
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