Add test 1342.

creusot-rs · Feb 5, 2025 · 0f9a60f · 0f9a60f
1 parent a3ecf47
commit 0f9a60f
Show file tree

Hide file tree

Showing 3 changed files with 51 additions and 0 deletions.
diff --git a/creusot/tests/should_succeed/bug/1342.coma b/creusot/tests/should_succeed/bug/1342.coma
diff --git a/creusot/tests/should_succeed/bug/1342.rs b/creusot/tests/should_succeed/bug/1342.rs
@@ -0,0 +1,13 @@
+extern crate creusot_contracts;
+use creusot_contracts::{logic::FSet, *};
+
+#[open]
+#[logic]
+#[variant(fset.len())]
+pub fn bar<T>(fset: FSet<T>) -> FSet<T> {
+    if fset.is_empty() {
+        FSet::EMPTY
+    } else {
+        bar(FSet::EMPTY)
+    }
+}
diff --git a/creusot/tests/should_succeed/bug/1342/proof.json b/creusot/tests/should_succeed/bug/1342/proof.json