diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-139.c
new file mode 100644
index 0000000000000000000000000000000000000000..d08b64bccfe85566d22503896fa2b3f8c381f67f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-139.c
@@ -0,0 +1,17 @@
+/* run.config_ci, run.config_dev
+   COMMENT: While unsupported, struct comparison should fail gracefully instead
+   COMMENT: of crashing Frama-C (issue frama-c/e-acsl#139).
+ */
+struct X {
+    int i ;
+};
+
+/*@ ensures *\old(item) == \old(*item); */
+void f(struct X *item){
+}
+
+int main() {
+    struct X x = {.i = 1};
+    f(&x);
+    return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-139.c
new file mode 100644
index 0000000000000000000000000000000000000000..4340159108fe6edec6394cdbb19468f3b4ac08bd
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-139.c
@@ -0,0 +1,56 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern int __e_acsl_sound_verdict;
+
+struct X {
+   int i ;
+};
+/*@ ensures *\old(item) ≡ \old(*item); */
+void __gen_e_acsl_f(struct X *item);
+
+void f(struct X *item)
+{
+  __e_acsl_store_block((void *)(& item),(size_t)8);
+  __e_acsl_delete_block((void *)(& item));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  struct X x = {.i = 1};
+  __e_acsl_store_block((void *)(& x),(size_t)4);
+  __e_acsl_full_init((void *)(& x));
+  __gen_e_acsl_f(& x);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& x));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+/*@ ensures *\old(item) ≡ \old(*item); */
+void __gen_e_acsl_f(struct X *item)
+{
+  struct X __gen_e_acsl_at_2;
+  struct X *__gen_e_acsl_at;
+  __e_acsl_store_block((void *)(& item),(size_t)8);
+  {
+    int __gen_e_acsl_valid_read;
+    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)item,
+                                                  sizeof(struct X),
+                                                  (void *)item,
+                                                  (void *)(& item));
+    __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+                    "mem_access: \\valid_read(item)",
+                    "tests/bts/issue-eacsl-139.c",9);
+    __gen_e_acsl_at_2 = *item;
+  }
+  __gen_e_acsl_at = item;
+  f(item);
+  __e_acsl_delete_block((void *)(& item));
+  return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-139.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-139.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ac3528903af3bd4f306a3e7a91c535efefa046e6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-139.res.oracle
@@ -0,0 +1,8 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/bts/issue-eacsl-139.c:9: Warning: 
+  E-ACSL construct `comparison between two structs or unions'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-139.c:9: Warning: 
+  function __gen_e_acsl_f: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-139.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-139.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391