Update tests

creusot-rs · Dec 3, 2024 · d285d5a · d285d5a
1 parent 78265c3
commit d285d5a
Show file tree

Hide file tree

Showing 51 changed files with 255 additions and 233 deletions.
diff --git a/creusot/tests/should_fail/bug/436_0.stderr b/creusot/tests/should_fail/bug/436_0.stderr
@@ -1,7 +1,7 @@
 error: called prophetic logic function `prophecy` in logic context
   --> 436_0.rs:15:23
    |
-15 |     b.g = snapshot! { prophecy(b) + 1i32 };
+15 |     b.g = snapshot! { prophecy(b) + 1 };
    |                       ^^^^^^^^
 
 error: aborting due to 1 previous error

diff --git a/creusot/tests/should_succeed/100doors.coma b/creusot/tests/should_succeed/100doors.coma
diff --git a/creusot/tests/should_succeed/bug/545.coma b/creusot/tests/should_succeed/bug/545.coma
diff --git a/creusot/tests/should_succeed/bug/545/why3session.xml b/creusot/tests/should_succeed/bug/545/why3session.xml
diff --git a/creusot/tests/should_succeed/bug/545/why3shapes.gz b/creusot/tests/should_succeed/bug/545/why3shapes.gz
diff --git a/creusot/tests/should_succeed/bug/682.coma b/creusot/tests/should_succeed/bug/682.coma
diff --git a/creusot/tests/should_succeed/bug/682/why3session.xml b/creusot/tests/should_succeed/bug/682/why3session.xml
diff --git a/creusot/tests/should_succeed/bug/682/why3shapes.gz b/creusot/tests/should_succeed/bug/682/why3shapes.gz
diff --git a/creusot/tests/should_succeed/bug/final_borrows.coma b/creusot/tests/should_succeed/bug/final_borrows.coma
diff --git a/creusot/tests/should_succeed/bug/two_phase.coma b/creusot/tests/should_succeed/bug/two_phase.coma
diff --git a/creusot/tests/should_succeed/cell/01.coma b/creusot/tests/should_succeed/cell/01.coma
diff --git a/creusot/tests/should_succeed/cell/01/why3shapes.gz b/creusot/tests/should_succeed/cell/01/why3shapes.gz
diff --git a/creusot/tests/should_succeed/cell/02.coma b/creusot/tests/should_succeed/cell/02.coma
diff --git a/creusot/tests/should_succeed/filter_positive.coma b/creusot/tests/should_succeed/filter_positive.coma
diff --git a/creusot/tests/should_succeed/ghost/ghost_vec.coma b/creusot/tests/should_succeed/ghost/ghost_vec.coma
diff --git a/creusot/tests/should_succeed/hashmap.coma b/creusot/tests/should_succeed/hashmap.coma