Skip to content

GitLab

why3
why3
Commit 2f4c5d86 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files
Options

ce oracle update

parent fd944728
Hide whitespace changes
Inline Side-by-side
Showing with 20 additions and 20 deletions
bench/ce/floats_Z3,4.6.0.oracle
View file @ 2f4c5d86
bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -11,7 +11,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g2: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -22,7 +22,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g3: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -32,7 +32,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -43,7 +43,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -54,7 +54,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g6: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -64,7 +64,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -75,7 +75,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g8: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -85,7 +85,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -96,7 +96,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g10: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -107,7 +107,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -118,7 +118,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g2: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -129,7 +129,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g3: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -139,7 +139,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -150,7 +150,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -161,7 +161,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g6: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -171,7 +171,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -182,7 +182,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g8: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -192,7 +192,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......@@ -203,7 +203,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g10: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
......
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