From 0f9a60fe6880d24f52595b0adebcedaf709ecf7f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@cnrs.fr>
Date: Wed, 5 Feb 2025 14:06:21 +0100
Subject: [PATCH] Add test 1342.

---
 creusot/tests/should_succeed/bug/1342.coma    | 27 +++++++++++++++++++
 creusot/tests/should_succeed/bug/1342.rs      | 13 +++++++++
 .../tests/should_succeed/bug/1342/proof.json  | 11 ++++++++
 3 files changed, 51 insertions(+)
 create mode 100644 creusot/tests/should_succeed/bug/1342.coma
 create mode 100644 creusot/tests/should_succeed/bug/1342.rs
 create mode 100644 creusot/tests/should_succeed/bug/1342/proof.json

diff --git a/creusot/tests/should_succeed/bug/1342.coma b/creusot/tests/should_succeed/bug/1342.coma
new file mode 100644
index 000000000..6c56cda22
--- /dev/null
+++ b/creusot/tests/should_succeed/bug/1342.coma
@@ -0,0 +1,27 @@
+module M_1342__bar [#"1342.rs" 7 0 7 39]
+  let%span s13420 = "1342.rs" 6 10 6 20
+  let%span s13421 = "1342.rs" 5 0 5 8
+  
+  use set.Fset
+  
+  type t_T'0
+  
+  use set.Fset
+  
+  use set.Fset
+  
+  use set.Fset
+  
+  use prelude.prelude.Int
+  
+  constant fset  : Fset.fset t_T'0
+  
+  function bar'0 [#"1342.rs" 7 0 7 39] (fset : Fset.fset t_T'0) : Fset.fset t_T'0
+  
+  goal vc_bar'0 : if Fset.is_empty fset then
+    true
+  else
+    0 <= ([%#s13420] Fset.cardinal fset)
+    /\ ([%#s13420] Fset.cardinal (Fset.empty : Fset.fset t_T'0)) < ([%#s13420] Fset.cardinal fset)
+
+end
diff --git a/creusot/tests/should_succeed/bug/1342.rs b/creusot/tests/should_succeed/bug/1342.rs
new file mode 100644
index 000000000..aaf9de979
--- /dev/null
+++ 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
new file mode 100644
index 000000000..b4bddc96d
--- /dev/null
+++ b/creusot/tests/should_succeed/bug/1342/proof.json
@@ -0,0 +1,11 @@
+{
+  "profile": [
+    { "prover": "z3@4.12.4", "size": 33, "time": 0.623 },
+    { "prover": "cvc5@1.0.5", "size": 46, "time": 0.533 },
+    { "prover": "alt-ergo@2.6.0", "size": 17, "time": 0.61 },
+    { "prover": "cvc4@1.8", "size": 45, "time": 0.426 }
+  ],
+  "proofs": {
+    "M_1342__bar": { "vc_bar'0": { "prover": "cvc5@1.0.5", "time": 0.034 } }
+  }
+}