From 64b9237dfc1ebad53809f7995bc68629d03b2c98 Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Tue, 2 Oct 2018 10:13:38 +0200
Subject: [PATCH] ce-bench: fix ce-bench
This updates values of already failing counterexamples which were changed
by the fix for z3/encoding_twin in 4b79dcf1e.
---
bench/ce/array_records_Z3,4.6.0.oracle | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/bench/ce/array_records_Z3,4.6.0.oracle b/bench/ce/array_records_Z3,4.6.0.oracle
index ad4504cfd..b63920279 100644
--- a/bench/ce/array_records_Z3,4.6.0.oracle
+++ b/bench/ce/array_records_Z3,4.6.0.oracle
@@ -110,17 +110,17 @@ bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
-"val" : "2" }
+"val" : "-176" }
Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
-"val" : "2" }
+"val" : "-176" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
-"val" : "2" }
+"val" : "-176" }
Line 25:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
-"val" : "2" }
+"val" : "-176" }
--
GitLab