diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
index 47566719f3..26c5a86bfa 100644
--- a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
+++ b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
@@ -5,25 +5,84 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -72,6 +131,12 @@
+
+
+
+
+
+
@@ -173,6 +238,12 @@
+
+
+
+
+
+
@@ -415,6 +486,14 @@
+
+
+
+
+
+
+
+
diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz
index 2f9588ccc6..693bb620f6 100644
Binary files a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz and b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz differ