diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index b02c5f9baca3095a13b63ba8a8e5c4bce77fbca5..66e0968c07197d14c9890358bdb3ca41895ed664 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -111,3 +111,16 @@ int main(void) {
 void test_f4() {
   /*@ assert f4 (0) ≡ 0; */
 }
+
+// same term \at(j, Old) twice in different typing contexts
+/*@
+  behavior a:
+    ensures 1 == -j;
+  behavior b:
+    ensures 2 == j;
+ */
+int f5(long int j) {}
+
+int test_f5() {
+  f5(1);
+}