diff --git a/Makefile.in b/Makefile.in index ba5f16b43c65f463052669295a4c3279e9057c84..47b374010f4ac6ba4e8c465ac304acb1e5974602 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1589,6 +1589,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \ # if test -d examples/runstrat ; then \ # $(MAKE) test-runstrat.@OCAMLBEST@ ; fi bash bench/bench ".@OCAMLBEST@" + @echo "" @if test "@enable_coq_tactic@" = "yes"; then \ echo "=== checking the Coq tactic ==="; \ $(MAKE) test-coq-tactic; fi diff --git a/bench/bench b/bench/bench index 57ba1ab53ced1f0597bf66976b5c2ba8a03d83c0..e1ef446b1851cf6174b89bbd696d82277f7009ed 100755 --- a/bench/bench +++ b/bench/bench @@ -254,3 +254,6 @@ list_stuff --list-formats list_stuff --list-metas list_stuff --list-debug-flags echo "" + +echo "=== Checking realizations ===" +exec bench/check_realizations.sh diff --git a/misc/check_realizations.sh b/bench/check_realizations.sh similarity index 100% rename from misc/check_realizations.sh rename to bench/check_realizations.sh diff --git a/misc/nightly-bench.sh b/misc/nightly-bench.sh index e988d48b87df4ef6f0627ab94f6d165c5834998d..3abca78e5610eac5c34e9fccbbd3f157cff2f029 100755 --- a/misc/nightly-bench.sh +++ b/misc/nightly-bench.sh @@ -137,9 +137,6 @@ else echo "Counterexample regression tests succeeded. " >> $REPORT fi -# check realizations -misc/check-realizations.sh >> $REPORT - # replay proofs examples/regtests.sh &> $OUT if test "$?" != "0" ; then