From 2f4c5d8634ad2bc2e543d11ded7552076082171b Mon Sep 17 00:00:00 2001 From: Sylvain Dailler <dailler@adacore.com> Date: Wed, 26 Sep 2018 12:50:00 +0200 Subject: [PATCH] ce oracle update --- bench/ce/floats_Z3,4.6.0.oracle | 40 ++++++++++++++++----------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/bench/ce/floats_Z3,4.6.0.oracle b/bench/ce/floats_Z3,4.6.0.oracle index 01dd18ff5..4a739da8e 100644 --- a/bench/ce/floats_Z3,4.6.0.oracle +++ b/bench/ce/floats_Z3,4.6.0.oracle @@ -1,6 +1,6 @@ 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: -- GitLab