Fix proofs.

creusot-rs · Dec 5, 2024 · 863b3a5 · 863b3a5
1 parent a080553
commit 863b3a5
Show file tree

Hide file tree

Showing 7 changed files with 139 additions and 125 deletions.
diff --git a/creusot/tests/should_succeed/hashmap.rs b/creusot/tests/should_succeed/hashmap.rs
@@ -46,7 +46,6 @@ impl<K: DeepModel, V> List<(K, V)> {
     }
 }
 
-
 impl<K: DeepModel, V> Resolve for List<(K, V)> {
     #[open(self)]
     #[predicate(prophetic)]

diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml
diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz b/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz
diff --git a/creusot/tests/should_succeed/iterators/05_map/why3session.xml b/creusot/tests/should_succeed/iterators/05_map/why3session.xml
diff --git a/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz b/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz
-Original file line number
+Diff line change
@@ Expand Up / @@ -46,7 +46,6 @@ impl<K: DeepModel, V> List<(K, V)> { @@
         }
     }
     impl<K: DeepModel, V> Resolve for List<(K, V)> {
         #[open(self)]
         #[predicate(prophetic)]
@@ Expand Down @@