diff --git a/tests/misc/asm_initialized.i b/tests/misc/asm_initialized.i
index d0be761ab181cbfe85b3d940bf76c0ae3f1c2d53..b0b3d60f4f4820d1157edd9136bf1c29fd26520e 100644
--- a/tests/misc/asm_initialized.i
+++ b/tests/misc/asm_initialized.i
@@ -5,7 +5,7 @@ STDOPT: #"-asm-contracts-ensure-init -asm-contracts-auto-validate -inline-stmt-c
 
 int main() {
   int* sp;
-  int x;
+  int x = 2;
   asm volatile ("mov %%rsp, %0;":"=r"(sp));
   *(sp - 2) = 3;
   return x;
diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle
index 86cf86de41f0c8e0e9518e089ad3507b61d1cd61..2d450df9513cfe5447010f99a6c95454dfd27dd3 100644
--- a/tests/misc/oracle/asm_initialized.res.oracle
+++ b/tests/misc/oracle/asm_initialized.res.oracle
@@ -8,15 +8,12 @@
   assertion 'inline_stmt_contract' got status unknown.
 [eva:alarm] asm_initialized.i:10: Warning: 
   out of bounds write. assert \valid(sp - 2);
-[eva:alarm] asm_initialized.i:11: Warning: 
-  accessing uninitialized left-value. assert \initialized(&x);
 [eva] Recording results for main
 [eva] Done for function main
-[eva] asm_initialized.i:11: 
-  assertion 'Eva,initialization' got final status invalid.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   NULL[rbits 2147483648 to 515396075527] ∈ [--..--]
+  x ∈ {2}
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -26,7 +23,7 @@
   \result FROM \nothing
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
-    NULL[268435456..4294967298]
+    NULL[268435456..4294967298]; x
 [inout] Inputs for function main:
     \nothing
 [report] Computing properties status...
@@ -43,9 +40,6 @@
             by inline_stmt_contract.
 [    -    ] Assertion 'Eva,mem_access' (file asm_initialized.i, line 10)
             tried with Eva.
-[  Alarm  ] Assertion 'Eva,initialization' (file asm_initialized.i, line 11)
-            By Eva, with pending:
-             - Unreachable return (file asm_initialized.i, line 11)
 [  Valid  ] Froms (file asm_initialized.i, line 9) at assembly (file asm_initialized.i, line 9)
             by asm_contracts.
 [  Valid  ] Default behavior at assembly (file asm_initialized.i, line 9)
@@ -56,14 +50,13 @@
 --------------------------------------------------------------------------------
      5 Completely validated
      1 To be validated
-     1 Alarm emitted
-     7 Total
+     6 Total
 --------------------------------------------------------------------------------
 /* Generated by Frama-C */
 int main(void)
 {
   int *sp;
-  int x;
+  int x = 2;
   /*@ ensures \initialized(&sp);
       assigns sp;
       assigns sp \from \nothing; */
@@ -71,7 +64,6 @@ int main(void)
   /*@ assert inline_stmt_contract: \initialized(&sp); */ ;
   /*@ assert Eva: mem_access: \valid(sp - 2); */
   *(sp - 2) = 3;
-  /*@ assert Eva: initialization: \initialized(&x); */
   return x;
 }