3 files changed, 19 insertions, 4 deletions
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 898af5590a..2439d3f378 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -31,16 +31,16 @@ coq_makefile -f _CoqProject -o Makefile
 make cleanall
 make make-pretty-timed-after TGTS="all" -j1 || exit $?
 rm -f time-of-build-before.log
-make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
+make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
 cp ../before/time-of-build-before.log ./
-make print-pretty-timed-diff || exit $?
+make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $?
 
 INFINITY="∞"
 INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase
 
 for ext in "" .desired; do
     for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
-	cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/  */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
+        cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/  */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
     done
 done
 for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
@@ -74,7 +74,7 @@ echo
 
 for ext in "" .desired; do
     for file in A.v.timing.diff; do
-	cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/  */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
+        cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/  */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
     done
 done
 for file in A.v.timing.diff; do
diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out
new file mode 100644
index 0000000000..94a0b19118
--- /dev/null
+++ b/test-suite/output/optimize_heap.out
@@ -0,0 +1,8 @@
+1 subgoal
+  
+  ============================
+  True
+1 subgoal
+  
+  ============================
+  True
diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v
new file mode 100644
index 0000000000..e566bd7bab
--- /dev/null
+++ b/test-suite/output/optimize_heap.v
@@ -0,0 +1,7 @@
+(* optimize_heap should not affect the proof state *)
+
+Goal True.
+  idtac.
+  Show.
+  optimize_heap.
+  Show.