From 904a1b6e9e2e023777a7a4b82ee7654828392817 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 30 Oct 2024 17:56:21 +0100
Subject: [PATCH] Update bench.

---
 bench/bench                           | 2 ++
 examples/tests/rac.oracle             | 2 +-
 examples/tests/replay/why3session.xml | 2 +-
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/bench/bench b/bench/bench
index 3ce346e6d..3591a5913 100755
--- a/bench/bench
+++ b/bench/bench
@@ -790,6 +790,7 @@ fi
 if enabled stackify && test -n "$has_stackify"; then
     echo "=== Checking stackify ==="
     replay examples/stackify --merging-only
+    echo ""
 fi
 
 
@@ -808,6 +809,7 @@ fi
 if enabled realizations; then
     echo "=== Checking realizations ==="
     bench/check_realizations.sh || exit $?
+    echo ""
 fi
 
 if enabled mlwprinter; then
diff --git a/examples/tests/rac.oracle b/examples/tests/rac.oracle
index 120f79482..1ecaf8cda 100644
--- a/examples/tests/rac.oracle
+++ b/examples/tests/rac.oracle
@@ -881,7 +881,7 @@ Loop variant decrease failed at "examples/tests/rac.mlw", line 510, characters 1
 * TestUInt64
 ** TestUInt64.test ()
 <rac:check_term_result>Postcondition of `max_uint64` is ok
-<rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/mach/int.mlw", line 610, characters 29-43
+<rac:check_term_result>Postcondition of `(+)` is ok at "WHY3DATA/stdlib/mach/int.mlw", line 612, characters 29-43
 <rac:check_term_result>Postcondition of `Tuple0` is ok at "command line expression to execute", line 1, characters 5-7
 <rac:check_term_result>Precondition of `(-)` failed at "examples/tests/rac.mlw", line 517, characters 16-21
                        - Defined at "WHY3DATA/stdlib/mach/int.mlw", line 67, characters 40-57
diff --git a/examples/tests/replay/why3session.xml b/examples/tests/replay/why3session.xml
index 17b966756..344c0e50b 100644
--- a/examples/tests/replay/why3session.xml
+++ b/examples/tests/replay/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="1" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="whyml">
 <path name=".."/><path name="replay.mlw"/>
 <theory name="Top">
-- 
2.11.4.GIT