diff --git a/tests/specs/oracle/ternary_op_bts1532.res.oracle b/tests/specs/oracle/ternary_op_bts1532.res.oracle
index 2421e2cd013a4542da3dc336b1810fb6ca9260dc..b00b48dca0fedc758f5b4228ead0f91836e249a9 100644
--- a/tests/specs/oracle/ternary_op_bts1532.res.oracle
+++ b/tests/specs/oracle/ternary_op_bts1532.res.oracle
@@ -1,11 +1,13 @@
 [kernel] Parsing tests/specs/ternary_op_bts1532.cpp (external front-end)
 Now output intermediate result
 /* Generated by Frama-C */
-/*@ ensures \result ≡ (1 ≢ 0? 2: 3); */
-_Bool empty(void)
+/*@ ensures \result ≡ (\old(x) ≢ 0? 0: 1); */
+_Bool empty(int x)
 {
   _Bool __retres;
-  __retres = (_Bool)1;
+  int tmp;
+  if ((_Bool)(x != 0)) tmp = 0; else tmp = 1;
+  __retres = (_Bool)(tmp != 0);
   return __retres;
 }
 
diff --git a/tests/specs/ternary_op_bts1532.cpp b/tests/specs/ternary_op_bts1532.cpp
index 43454b19e1276f4f6cb21fcb0583b52d18d6a386..3352d561007e17005c4ce72e23ce5cdcd577ba38 100644
--- a/tests/specs/ternary_op_bts1532.cpp
+++ b/tests/specs/ternary_op_bts1532.cpp
@@ -1,6 +1,6 @@
 
-//@ ensures \result == (1 ? 2 : 3);
-bool empty() { return (1 ? 2 : 3); }
+//@ ensures \result == (x ? 0 : 1);
+bool empty(int x) { return (x ? 0 : 1); }
 
 //@ logic integer min(integer x, integer y) = x < y ? x : y;