diff --git a/tests/value/oracle/recursion.0.res.oracle b/tests/value/oracle/recursion.0.res.oracle
index ce21d446188bb4c6d799e48dd493768b5edd735b..44eff474189c5c7e9ef609d0707957df7b0b60b1 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -5,256 +5,256 @@
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
   p ∈ {0}
-[eva:recursion] tests/value/recursion.c:18: 
+[eva:recursion] tests/value/recursion.c:21: 
   detected recursive call of function five.
-[eva] tests/value/recursion.c:18: Warning: 
+[eva] tests/value/recursion.c:21: Warning: 
   Using specification of function five for recursive calls.
   Analysis of function five is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function five
-[eva:alarm] tests/value/recursion.c:15: Warning: 
+[eva:alarm] tests/value/recursion.c:18: Warning: 
   function five: postcondition got status unknown.
-[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
-[eva:recursion] tests/value/recursion.c:28: 
+[eva] tests/value/recursion.c:345: Frama_C_show_each_5: {5}
+[eva:recursion] tests/value/recursion.c:31: 
   detected recursive call of function sum.
-[eva] tests/value/recursion.c:28: Warning: 
+[eva] tests/value/recursion.c:31: Warning: 
   Using specification of function sum for recursive calls.
   Analysis of function sum is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function sum
-[eva:alarm] tests/value/recursion.c:24: Warning: 
+[eva:alarm] tests/value/recursion.c:27: Warning: 
   function sum: postcondition got status unknown.
-[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
-[eva:recursion] tests/value/recursion.c:37: 
+[eva] tests/value/recursion.c:347: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:40: 
   detected recursive call of function factorial.
-[eva] tests/value/recursion.c:37: Warning: 
+[eva] tests/value/recursion.c:40: Warning: 
   Using specification of function factorial for recursive calls.
   Analysis of function factorial is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function factorial
-[eva] tests/value/recursion.c:346: Frama_C_show_each_120: [0..4294967295]
-[eva:recursion] tests/value/recursion.c:46: 
+[eva] tests/value/recursion.c:349: Frama_C_show_each_120: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:49: 
   detected recursive call of function syracuse.
-[eva] tests/value/recursion.c:46: Warning: 
+[eva] tests/value/recursion.c:49: Warning: 
   Using specification of function syracuse for recursive calls.
   Analysis of function syracuse is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function syracuse
-[eva] tests/value/recursion.c:348: Frama_C_show_each_1: [0..4294967294]
-[eva:recursion] tests/value/recursion.c:59: 
+[eva] tests/value/recursion.c:351: Frama_C_show_each_1: [0..4294967294]
+[eva:recursion] tests/value/recursion.c:62: 
   detected recursive call of function fibonacci.
-[eva] tests/value/recursion.c:59: Warning: 
+[eva] tests/value/recursion.c:62: Warning: 
   Using specification of function fibonacci for recursive calls.
   Analysis of function fibonacci is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function fibonacci
-[eva:recursion] tests/value/recursion.c:60: 
+[eva:recursion] tests/value/recursion.c:63: 
   detected recursive call of function fibonacci.
-[eva] tests/value/recursion.c:60: Warning: 
+[eva] tests/value/recursion.c:63: Warning: 
   Using specification of function fibonacci for recursive calls.
   Analysis of function fibonacci is thus incomplete and its soundness
   relies on the written specification.
-[eva] tests/value/recursion.c:350: Frama_C_show_each_89: [0..4294967295]
-[eva:recursion] tests/value/recursion.c:76: 
+[eva] tests/value/recursion.c:353: Frama_C_show_each_89: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:79: 
   detected recursive call of function sum_ptr.
-[eva] tests/value/recursion.c:76: Warning: 
+[eva] tests/value/recursion.c:79: Warning: 
   Using specification of function sum_ptr for recursive calls.
   Analysis of function sum_ptr is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function sum_ptr
-[eva:alarm] tests/value/recursion.c:68: Warning: 
+[eva:alarm] tests/value/recursion.c:71: Warning: 
   function sum_ptr: postcondition got status unknown.
-[eva:alarm] tests/value/recursion.c:69: Warning: 
+[eva:alarm] tests/value/recursion.c:72: Warning: 
   function sum_ptr: postcondition got status unknown.
-[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
-[eva:recursion] tests/value/recursion.c:89: 
+[eva] tests/value/recursion.c:358: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:92: 
   detected recursive call of function factorial_ptr.
-[eva] tests/value/recursion.c:89: Warning: 
+[eva] tests/value/recursion.c:92: Warning: 
   Using specification of function factorial_ptr for recursive calls.
   Analysis of function factorial_ptr is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function factorial_ptr
-[eva:alarm] tests/value/recursion.c:90: Warning: 
+[eva:alarm] tests/value/recursion.c:93: Warning: 
   accessing uninitialized left-value. assert \initialized(&res);
-[eva] tests/value/recursion.c:358: Frama_C_show_each_120: [0..4294967295]
-[eva:recursion] tests/value/recursion.c:101: 
+[eva] tests/value/recursion.c:361: Frama_C_show_each_120: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:104: 
   detected recursive call of function syracuse_ptr.
-[eva] tests/value/recursion.c:101: Warning: 
+[eva] tests/value/recursion.c:104: Warning: 
   Using specification of function syracuse_ptr for recursive calls.
   Analysis of function syracuse_ptr is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function syracuse_ptr
-[eva:alarm] tests/value/recursion.c:102: Warning: 
+[eva:alarm] tests/value/recursion.c:105: Warning: 
   accessing uninitialized left-value. assert \initialized(&prev_res);
-[eva] tests/value/recursion.c:361: Frama_C_show_each_1: [0..4294967294]
-[eva:recursion] tests/value/recursion.c:117: 
+[eva] tests/value/recursion.c:364: Frama_C_show_each_1: [0..4294967294]
+[eva:recursion] tests/value/recursion.c:120: 
   detected recursive call of function fibonacci_ptr.
-[eva] tests/value/recursion.c:117: Warning: 
+[eva] tests/value/recursion.c:120: Warning: 
   Using specification of function fibonacci_ptr for recursive calls.
   Analysis of function fibonacci_ptr is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function fibonacci_ptr
-[eva:recursion] tests/value/recursion.c:119: 
+[eva:recursion] tests/value/recursion.c:122: 
   detected recursive call of function fibonacci_ptr.
-[eva] tests/value/recursion.c:119: Warning: 
+[eva] tests/value/recursion.c:122: Warning: 
   Using specification of function fibonacci_ptr for recursive calls.
   Analysis of function fibonacci_ptr is thus incomplete and its soundness
   relies on the written specification.
-[eva:alarm] tests/value/recursion.c:120: Warning: 
+[eva:alarm] tests/value/recursion.c:123: Warning: 
   accessing uninitialized left-value. assert \initialized(&x);
-[eva:alarm] tests/value/recursion.c:120: Warning: 
+[eva:alarm] tests/value/recursion.c:123: Warning: 
   accessing uninitialized left-value. assert \initialized(&y);
-[eva] tests/value/recursion.c:364: Frama_C_show_each_89: [0..4294967295]
-[eva:recursion] tests/value/recursion.c:137: 
+[eva] tests/value/recursion.c:367: Frama_C_show_each_89: [0..4294967295]
+[eva:recursion] tests/value/recursion.c:140: 
   detected recursive call of function sum_and_fact.
-[eva] tests/value/recursion.c:137: Warning: 
+[eva] tests/value/recursion.c:140: Warning: 
   Using specification of function sum_and_fact for recursive calls.
   Analysis of function sum_and_fact is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function sum_and_fact
-[eva:alarm] tests/value/recursion.c:128: Warning: 
+[eva:alarm] tests/value/recursion.c:131: Warning: 
   function sum_and_fact: postcondition got status unknown.
-[eva:alarm] tests/value/recursion.c:129: Warning: 
+[eva:alarm] tests/value/recursion.c:132: Warning: 
   function sum_and_fact: postcondition got status unknown.
-[eva] tests/value/recursion.c:368: 
+[eva] tests/value/recursion.c:371: 
   Frama_C_show_each_36_40320: {36}, [0..4294967288],0%8
-[eva:recursion] tests/value/recursion.c:161: 
+[eva:recursion] tests/value/recursion.c:164: 
   detected recursive call of function odd.
-[eva] tests/value/recursion.c:161: Warning: 
+[eva] tests/value/recursion.c:164: Warning: 
   Using specification of function odd for recursive calls.
   Analysis of function odd is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function odd
-[eva:alarm] tests/value/recursion.c:149: Warning: 
+[eva:alarm] tests/value/recursion.c:152: Warning: 
   function odd: postcondition got status unknown.
-[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
-[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
-[eva:recursion] tests/value/recursion.c:183: 
+[eva] tests/value/recursion.c:376: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:379: Frama_C_show_each_0: {0}, {0}
+[eva:recursion] tests/value/recursion.c:186: 
   detected recursive call of function odd_ptr.
-[eva] tests/value/recursion.c:183: Warning: 
+[eva] tests/value/recursion.c:186: Warning: 
   Using specification of function odd_ptr for recursive calls.
   Analysis of function odd_ptr is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function odd_ptr
-[eva:alarm] tests/value/recursion.c:167: Warning: 
+[eva:alarm] tests/value/recursion.c:170: Warning: 
   function odd_ptr: postcondition got status unknown.
-[eva:alarm] tests/value/recursion.c:184: Warning: 
+[eva:alarm] tests/value/recursion.c:187: Warning: 
   accessing uninitialized left-value. assert \initialized(&y);
-[eva:alarm] tests/value/recursion.c:179: Warning: 
+[eva:alarm] tests/value/recursion.c:182: Warning: 
   function even_ptr: postcondition got status unknown.
-[eva:recursion] tests/value/recursion.c:171: 
+[eva:recursion] tests/value/recursion.c:174: 
   detected recursive call of function even_ptr.
-[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
-[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
+[eva] tests/value/recursion.c:382: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:385: Frama_C_show_each_0: {0}, {0}
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
 [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
-[eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [0..4294967295]
+[eva] tests/value/recursion.c:394: Frama_C_show_each_6_66: [6..66]
 [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [0..4294967295]
-[eva:alarm] tests/value/recursion.c:222: Warning: 
+[eva] tests/value/recursion.c:400: Frama_C_show_each_2_89: [0..4294967295]
+[eva:alarm] tests/value/recursion.c:225: Warning: 
   function fill_array: precondition got status invalid.
-[eva:alarm] tests/value/recursion.c:226: Warning: 
+[eva:alarm] tests/value/recursion.c:229: Warning: 
   function fill_array: precondition got status unknown.
-[eva:recursion] tests/value/recursion.c:200: 
+[eva:recursion] tests/value/recursion.c:203: 
   detected recursive call of function fill_array.
-[eva] tests/value/recursion.c:200: Warning: 
+[eva] tests/value/recursion.c:203: Warning: 
   Using specification of function fill_array for recursive calls.
   Analysis of function fill_array is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function fill_array
-[eva:alarm] tests/value/recursion.c:200: Warning: 
+[eva:alarm] tests/value/recursion.c:203: Warning: 
   function fill_array: precondition got status unknown.
-[eva:alarm] tests/value/recursion.c:194: Warning: 
+[eva:alarm] tests/value/recursion.c:197: Warning: 
   function fill_array: postcondition got status unknown.
-[eva:alarm] tests/value/recursion.c:228: Warning: 
+[eva:alarm] tests/value/recursion.c:231: Warning: 
   function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
-[eva:recursion] tests/value/recursion.c:214: 
+[eva:recursion] tests/value/recursion.c:217: 
   detected recursive call of function binary_search.
-[eva] tests/value/recursion.c:214: Warning: 
+[eva] tests/value/recursion.c:217: Warning: 
   Using specification of function binary_search for recursive calls.
   Analysis of function binary_search is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function binary_search
-[eva:recursion] tests/value/recursion.c:216: 
+[eva:recursion] tests/value/recursion.c:219: 
   detected recursive call of function binary_search.
-[eva] tests/value/recursion.c:216: Warning: 
+[eva] tests/value/recursion.c:219: Warning: 
   Using specification of function binary_search for recursive calls.
   Analysis of function binary_search is thus incomplete and its soundness
   relies on the written specification.
-[eva] tests/value/recursion.c:229: 
+[eva] tests/value/recursion.c:232: 
   Frama_C_show_each_3: [-2147483648..2147483647]
-[eva] tests/value/recursion.c:231: 
+[eva] tests/value/recursion.c:234: 
   Frama_C_show_each_12: [-2147483648..2147483647]
-[eva] tests/value/recursion.c:233: 
+[eva] tests/value/recursion.c:236: 
   Frama_C_show_each_minus1: [-2147483648..2147483647]
-[eva] tests/value/recursion.c:238: 
-  Frama_C_show_each_7_11: [-2147483648..2147483647]
 [eva] tests/value/recursion.c:241: 
+  Frama_C_show_each_7_11: [-2147483648..2147483647]
+[eva] tests/value/recursion.c:244: 
   Frama_C_show_each_minus_1_15: [-2147483648..2147483647]
-[eva:recursion] tests/value/recursion.c:252: 
+[eva:recursion] tests/value/recursion.c:255: 
   detected recursive call of function alarm.
-[eva] tests/value/recursion.c:252: Warning: 
+[eva] tests/value/recursion.c:255: Warning: 
   Using specification of function alarm for recursive calls.
   Analysis of function alarm is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function alarm
-[eva:alarm] tests/value/recursion.c:247: Warning: 
+[eva:alarm] tests/value/recursion.c:250: Warning: 
   function alarm: postcondition got status unknown.
-[eva:alarm] tests/value/recursion.c:252: Warning: 
+[eva:alarm] tests/value/recursion.c:255: Warning: 
   signed overflow. assert i * tmp ≤ 2147483647;
                    (tmp from alarm(i - 1))
-[eva] tests/value/recursion.c:406: 
+[eva] tests/value/recursion.c:409: 
   Frama_C_show_each_unreachable: [20..2147483640],0%20
-[eva:recursion] tests/value/recursion.c:261: 
+[eva:recursion] tests/value/recursion.c:264: 
   detected recursive call of function precond.
-[eva] tests/value/recursion.c:261: Warning: 
+[eva] tests/value/recursion.c:264: Warning: 
   Using specification of function precond for recursive calls.
   Analysis of function precond is thus incomplete and its soundness
   relies on the written specification.
 [inout] Warning: no assigns clauses for function precond.
   Results will be imprecise.
 [eva] using specification for function precond
-[eva] tests/value/recursion.c:261: Warning: 
+[eva] tests/value/recursion.c:264: Warning: 
   Cannot handle empty assigns clause. Assuming assigns \nothing: be aware this is probably incorrect.
-[eva:recursion] tests/value/recursion.c:276: 
+[eva:recursion] tests/value/recursion.c:279: 
   detected recursive call of function escaping_local.
-[eva] tests/value/recursion.c:276: Warning: 
+[eva] tests/value/recursion.c:279: Warning: 
   Using specification of function escaping_local for recursive calls.
   Analysis of function escaping_local is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function escaping_local
-[eva:alarm] tests/value/recursion.c:278: Warning: 
+[eva:alarm] tests/value/recursion.c:281: Warning: 
   out of bounds write. assert \valid(p);
-[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {5}
-[eva:locals-escaping] tests/value/recursion.c:277: Warning: 
+[eva] tests/value/recursion.c:282: Frama_C_show_each_1: {5}
+[eva:locals-escaping] tests/value/recursion.c:280: Warning: 
   locals {x} escaping the scope of a block of escaping_local through p
-[eva:recursion] tests/value/recursion.c:291: 
+[eva:recursion] tests/value/recursion.c:294: 
   detected recursive call of function escaping_formal.
-[eva] tests/value/recursion.c:291: Warning: 
+[eva] tests/value/recursion.c:294: Warning: 
   Using specification of function escaping_formal for recursive calls.
   Analysis of function escaping_formal is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function escaping_formal
-[eva:alarm] tests/value/recursion.c:293: Warning: 
+[eva:alarm] tests/value/recursion.c:296: Warning: 
   out of bounds write. assert \valid(p);
-[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {5}
-[eva:locals-escaping] tests/value/recursion.c:411: Warning: 
+[eva] tests/value/recursion.c:297: Frama_C_show_each_1: {5}
+[eva:locals-escaping] tests/value/recursion.c:414: Warning: 
   locals {x} escaping the scope of escaping_formal through p
-[eva:recursion] tests/value/recursion.c:307: 
+[eva:recursion] tests/value/recursion.c:310: 
   detected recursive call of function escaping_stack.
-[eva] tests/value/recursion.c:307: Warning: 
+[eva] tests/value/recursion.c:310: Warning: 
   Using specification of function escaping_stack for recursive calls.
   Analysis of function escaping_stack is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function escaping_stack
-[eva:alarm] tests/value/recursion.c:309: Warning: 
+[eva:alarm] tests/value/recursion.c:312: Warning: 
   out of bounds write. assert \valid(p);
-[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {5}
-[eva:locals-escaping] tests/value/recursion.c:308: Warning: 
+[eva] tests/value/recursion.c:313: Frama_C_show_each_1_2: {5}
+[eva:locals-escaping] tests/value/recursion.c:311: Warning: 
   locals {x} escaping the scope of a block of escaping_stack through p
-[eva:recursion] tests/value/recursion.c:323: 
+[eva:recursion] tests/value/recursion.c:326: 
   detected recursive call of function decr.
-[eva] tests/value/recursion.c:323: Warning: 
+[eva] tests/value/recursion.c:326: Warning: 
   Using specification of function decr for recursive calls.
   Analysis of function decr is thus incomplete and its soundness
   relies on the written specification.
@@ -276,7 +276,7 @@
 [eva:final-states] Values at end of function escaping_stack:
   p ∈
    {{ garbled mix of &{a}
-    (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
+    (origin: Library function {tests/value/recursion.c:310}) }} or ESCAPINGADDR
   a ∈ [--..--]
 [eva:final-states] Values at end of function even:
   __retres ∈ UNINITIALIZED
@@ -349,7 +349,7 @@ Cannot filter: dumping raw memory (including unchanged variables)
   nondet ∈ [--..--]
   p ∈
    {{ garbled mix of &{a}
-    (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
+    (origin: Library function {tests/value/recursion.c:310}) }} or ESCAPINGADDR
   a ∈ [--..--]
   b ∈ {0}
   x ∈ [10..20]
diff --git a/tests/value/oracle/recursion.1.res.oracle b/tests/value/oracle/recursion.1.res.oracle
index 5fd6d46ceb18ba3e3efda9e41353d2e7da7de780..48c525beac41514630ef0799a910ccd98fce7dde 100644
--- a/tests/value/oracle/recursion.1.res.oracle
+++ b/tests/value/oracle/recursion.1.res.oracle
@@ -5,136 +5,136 @@
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
   p ∈ {0}
-[eva:recursion] tests/value/recursion.c:18: 
+[eva:recursion] tests/value/recursion.c:21: 
   detected recursive call of function five.
-[eva] tests/value/recursion.c:18: Warning: 
+[eva] tests/value/recursion.c:21: Warning: 
   Using specification of function five for recursive calls of depth 20.
   Analysis of function five is thus incomplete and its soundness
   relies on the written specification.
 [eva] using specification for function five
-[eva:alarm] tests/value/recursion.c:15: Warning: 
+[eva:alarm] tests/value/recursion.c:18: Warning: 
   function five: postcondition got status unknown.
-[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
-[eva:recursion] tests/value/recursion.c:28: 
+[eva] tests/value/recursion.c:345: Frama_C_show_each_5: {5}
+[eva:recursion] tests/value/recursion.c:31: 
   detected recursive call of function sum.
-[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
-[eva:recursion] tests/value/recursion.c:37: 
+[eva] tests/value/recursion.c:347: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:40: 
   detected recursive call of function factorial.
-[eva] tests/value/recursion.c:346: Frama_C_show_each_120: {120}
-[eva:recursion] tests/value/recursion.c:46: 
+[eva] tests/value/recursion.c:349: Frama_C_show_each_120: {120}
+[eva:recursion] tests/value/recursion.c:49: 
   detected recursive call of function syracuse.
-[eva] tests/value/recursion.c:348: Frama_C_show_each_1: {1}
-[eva:recursion] tests/value/recursion.c:59: 
+[eva] tests/value/recursion.c:351: Frama_C_show_each_1: {1}
+[eva:recursion] tests/value/recursion.c:62: 
   detected recursive call of function fibonacci.
-[eva:recursion] tests/value/recursion.c:60: 
+[eva:recursion] tests/value/recursion.c:63: 
   detected recursive call of function fibonacci.
-[eva] tests/value/recursion.c:350: Frama_C_show_each_89: {89}
-[eva:recursion] tests/value/recursion.c:76: 
+[eva] tests/value/recursion.c:353: Frama_C_show_each_89: {89}
+[eva:recursion] tests/value/recursion.c:79: 
   detected recursive call of function sum_ptr.
-[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
-[eva:recursion] tests/value/recursion.c:89: 
+[eva] tests/value/recursion.c:358: Frama_C_show_each_91: {91}
+[eva:recursion] tests/value/recursion.c:92: 
   detected recursive call of function factorial_ptr.
-[eva] tests/value/recursion.c:358: Frama_C_show_each_120: {120}
-[eva:recursion] tests/value/recursion.c:101: 
+[eva] tests/value/recursion.c:361: Frama_C_show_each_120: {120}
+[eva:recursion] tests/value/recursion.c:104: 
   detected recursive call of function syracuse_ptr.
-[eva] tests/value/recursion.c:361: Frama_C_show_each_1: {1}
-[eva:recursion] tests/value/recursion.c:117: 
+[eva] tests/value/recursion.c:364: Frama_C_show_each_1: {1}
+[eva:recursion] tests/value/recursion.c:120: 
   detected recursive call of function fibonacci_ptr.
-[eva:recursion] tests/value/recursion.c:119: 
+[eva:recursion] tests/value/recursion.c:122: 
   detected recursive call of function fibonacci_ptr.
-[eva] tests/value/recursion.c:364: Frama_C_show_each_89: {89}
-[eva:recursion] tests/value/recursion.c:137: 
+[eva] tests/value/recursion.c:367: Frama_C_show_each_89: {89}
+[eva:recursion] tests/value/recursion.c:140: 
   detected recursive call of function sum_and_fact.
-[eva] tests/value/recursion.c:368: Frama_C_show_each_36_40320: {36}, {40320}
-[eva:recursion] tests/value/recursion.c:161: 
+[eva] tests/value/recursion.c:371: Frama_C_show_each_36_40320: {36}, {40320}
+[eva:recursion] tests/value/recursion.c:164: 
   detected recursive call of function odd.
-[eva:recursion] tests/value/recursion.c:152: 
+[eva:recursion] tests/value/recursion.c:155: 
   detected recursive call of function even.
-[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
-[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
-[eva:recursion] tests/value/recursion.c:183: 
+[eva] tests/value/recursion.c:376: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:379: Frama_C_show_each_0: {0}, {0}
+[eva:recursion] tests/value/recursion.c:186: 
   detected recursive call of function odd_ptr.
-[eva:recursion] tests/value/recursion.c:171: 
+[eva:recursion] tests/value/recursion.c:174: 
   detected recursive call of function even_ptr.
-[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
-[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
+[eva] tests/value/recursion.c:382: Frama_C_show_each_1: {1}, {1}
+[eva] tests/value/recursion.c:385: Frama_C_show_each_0: {0}, {0}
 [eva] using specification for function Frama_C_interval
-[eva:alarm] tests/value/recursion.c:24: Warning: 
+[eva:alarm] tests/value/recursion.c:27: Warning: 
   function sum: postcondition got status unknown.
-[eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
-[eva:alarm] tests/value/recursion.c:69: Warning: 
-  function sum_ptr: postcondition got status unknown.
 [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
-[eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [2..89]
+[eva:alarm] tests/value/recursion.c:72: Warning: 
+  function sum_ptr: postcondition got status unknown.
+[eva] tests/value/recursion.c:394: Frama_C_show_each_6_66: [6..66]
 [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [2..89]
-[eva:alarm] tests/value/recursion.c:222: Warning: 
+[eva] tests/value/recursion.c:400: Frama_C_show_each_2_89: [2..89]
+[eva:alarm] tests/value/recursion.c:225: Warning: 
   function fill_array: precondition got status invalid.
-[eva:alarm] tests/value/recursion.c:226: Warning: 
+[eva:alarm] tests/value/recursion.c:229: Warning: 
   function fill_array: precondition got status unknown.
-[eva:recursion] tests/value/recursion.c:200: 
+[eva:recursion] tests/value/recursion.c:203: 
   detected recursive call of function fill_array.
-[eva:alarm] tests/value/recursion.c:200: Warning: 
+[eva:alarm] tests/value/recursion.c:203: Warning: 
   function fill_array: precondition got status unknown.
-[eva:alarm] tests/value/recursion.c:199: Warning: 
+[eva:alarm] tests/value/recursion.c:202: Warning: 
   out of bounds write. assert \valid(data + start);
-[kernel] tests/value/recursion.c:199: Warning: 
+[kernel] tests/value/recursion.c:202: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva:alarm] tests/value/recursion.c:194: Warning: 
+[eva:alarm] tests/value/recursion.c:197: Warning: 
   function fill_array: postcondition got status unknown.
-[eva:alarm] tests/value/recursion.c:228: Warning: 
+[eva:alarm] tests/value/recursion.c:231: Warning: 
   function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
-[eva:recursion] tests/value/recursion.c:214: 
+[eva:recursion] tests/value/recursion.c:217: 
   detected recursive call of function binary_search.
-[eva] tests/value/recursion.c:229: Frama_C_show_each_3: {3}
-[eva:recursion] tests/value/recursion.c:216: 
+[eva] tests/value/recursion.c:232: Frama_C_show_each_3: {3}
+[eva:recursion] tests/value/recursion.c:219: 
   detected recursive call of function binary_search.
-[eva] tests/value/recursion.c:231: Frama_C_show_each_12: {12}
-[eva] tests/value/recursion.c:233: Frama_C_show_each_minus1: {-1}
-[eva] tests/value/recursion.c:238: Frama_C_show_each_7_11: {7; 8; 9; 10; 11}
-[eva] tests/value/recursion.c:241: Frama_C_show_each_minus_1_15: [-1..15]
-[eva:recursion] tests/value/recursion.c:252: 
+[eva] tests/value/recursion.c:234: Frama_C_show_each_12: {12}
+[eva] tests/value/recursion.c:236: Frama_C_show_each_minus1: {-1}
+[eva] tests/value/recursion.c:241: Frama_C_show_each_7_11: {7; 8; 9; 10; 11}
+[eva] tests/value/recursion.c:244: Frama_C_show_each_minus_1_15: [-1..15]
+[eva:recursion] tests/value/recursion.c:255: 
   detected recursive call of function alarm.
-[eva:alarm] tests/value/recursion.c:252: Warning: 
+[eva:alarm] tests/value/recursion.c:255: Warning: 
   signed overflow. assert i * tmp ≤ 2147483647;
                    (tmp from alarm(i - 1))
-[eva:recursion] tests/value/recursion.c:261: 
+[eva:recursion] tests/value/recursion.c:264: 
   detected recursive call of function precond.
-[eva:alarm] tests/value/recursion.c:261: Warning: 
+[eva:alarm] tests/value/recursion.c:264: Warning: 
   function precond: precondition got status invalid.
-[eva:recursion] tests/value/recursion.c:276: 
+[eva:recursion] tests/value/recursion.c:279: 
   detected recursive call of function escaping_local.
-[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {1}
-[eva:locals-escaping] tests/value/recursion.c:277: Warning: 
+[eva] tests/value/recursion.c:282: Frama_C_show_each_1: {1}
+[eva:locals-escaping] tests/value/recursion.c:280: Warning: 
   locals {x} escaping the scope of a block of escaping_local through p
-[eva:alarm] tests/value/recursion.c:278: Warning: 
+[eva:alarm] tests/value/recursion.c:281: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(&p);
-[kernel] tests/value/recursion.c:278: Warning: 
+[kernel] tests/value/recursion.c:281: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva:recursion] tests/value/recursion.c:291: 
+[eva:recursion] tests/value/recursion.c:294: 
   detected recursive call of function escaping_formal.
-[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {1}
-[eva:locals-escaping] tests/value/recursion.c:291: Warning: 
+[eva] tests/value/recursion.c:297: Frama_C_show_each_1: {1}
+[eva:locals-escaping] tests/value/recursion.c:294: Warning: 
   locals {x} escaping the scope of escaping_formal through p
-[eva:alarm] tests/value/recursion.c:293: Warning: 
+[eva:alarm] tests/value/recursion.c:296: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(&p);
-[kernel] tests/value/recursion.c:293: Warning: 
+[kernel] tests/value/recursion.c:296: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva:recursion] tests/value/recursion.c:307: 
+[eva:recursion] tests/value/recursion.c:310: 
   detected recursive call of function escaping_stack.
-[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {1}
-[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {2}
-[eva:locals-escaping] tests/value/recursion.c:308: Warning: 
+[eva] tests/value/recursion.c:313: Frama_C_show_each_1_2: {1}
+[eva] tests/value/recursion.c:313: Frama_C_show_each_1_2: {2}
+[eva:locals-escaping] tests/value/recursion.c:311: Warning: 
   locals {x} escaping the scope of a block of escaping_stack through p
-[eva:alarm] tests/value/recursion.c:309: Warning: 
+[eva:alarm] tests/value/recursion.c:312: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(&p);
-[kernel] tests/value/recursion.c:309: Warning: 
+[kernel] tests/value/recursion.c:312: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
-[eva:recursion] tests/value/recursion.c:323: 
+[eva:recursion] tests/value/recursion.c:326: 
   detected recursive call of function decr.
-[eva] tests/value/recursion.c:323: Warning: 
+[eva] tests/value/recursion.c:326: Warning: 
   Using specification of function decr for recursive calls of depth 20.
   Analysis of function decr is thus incomplete and its soundness
   relies on the written specification.
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
index c4c6916fda19c0763ef4ab50cc3d834a54df296a..f4e323985bd2d733470e0b542cf2b13ce88e8bcc 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -5,12 +5,12 @@
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
   p ∈ {0}
-[eva:recursion] tests/value/recursion.c:422: 
+[eva:recursion] tests/value/recursion.c:425: 
   detected recursive call of function sum_nospec.
-[eva] tests/value/recursion.c:429: Frama_C_show_each_10: {10}
-[eva] tests/value/recursion.c:434: Frama_C_show_each_36: {36}
+[eva] tests/value/recursion.c:432: Frama_C_show_each_10: {10}
+[eva] tests/value/recursion.c:437: Frama_C_show_each_36: {36}
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/recursion.c:422: User Error: 
+[eva] tests/value/recursion.c:425: User Error: 
   Recursive call to sum_nospec without a specification. Try to increase
   the -eva-unroll-recursive-calls parameter or write a specification
   for function sum_nospec.
diff --git a/tests/value/oracle_apron/recursion.0.res.oracle b/tests/value/oracle_apron/recursion.0.res.oracle
deleted file mode 100644
index 424fb0f10c57946bd4a9bf10e95994d708e89a4a..0000000000000000000000000000000000000000
--- a/tests/value/oracle_apron/recursion.0.res.oracle
+++ /dev/null
@@ -1,628 +0,0 @@
-10,632c10,12
-< [eva] tests/value/recursion.c:18: Warning: 
-<   Using specification of function five for recursive calls.
-<   Analysis of function five is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function five
-< [eva:alarm] tests/value/recursion.c:15: Warning: 
-<   function five: postcondition got status unknown.
-< [eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
-< [eva:recursion] tests/value/recursion.c:28: 
-<   detected recursive call of function sum.
-< [eva] tests/value/recursion.c:28: Warning: 
-<   Using specification of function sum for recursive calls.
-<   Analysis of function sum is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function sum
-< [eva:alarm] tests/value/recursion.c:24: Warning: 
-<   function sum: postcondition got status unknown.
-< [eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
-< [eva:recursion] tests/value/recursion.c:37: 
-<   detected recursive call of function factorial.
-< [eva] tests/value/recursion.c:37: Warning: 
-<   Using specification of function factorial for recursive calls.
-<   Analysis of function factorial is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function factorial
-< [eva] tests/value/recursion.c:346: Frama_C_show_each_120: [0..4294967295]
-< [eva:recursion] tests/value/recursion.c:46: 
-<   detected recursive call of function syracuse.
-< [eva] tests/value/recursion.c:46: Warning: 
-<   Using specification of function syracuse for recursive calls.
-<   Analysis of function syracuse is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function syracuse
-< [eva] tests/value/recursion.c:348: Frama_C_show_each_1: [0..4294967294]
-< [eva:recursion] tests/value/recursion.c:59: 
-<   detected recursive call of function fibonacci.
-< [eva] tests/value/recursion.c:59: Warning: 
-<   Using specification of function fibonacci for recursive calls.
-<   Analysis of function fibonacci is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function fibonacci
-< [eva:recursion] tests/value/recursion.c:60: 
-<   detected recursive call of function fibonacci.
-< [eva] tests/value/recursion.c:60: Warning: 
-<   Using specification of function fibonacci for recursive calls.
-<   Analysis of function fibonacci is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] tests/value/recursion.c:350: Frama_C_show_each_89: [0..4294967295]
-< [eva:recursion] tests/value/recursion.c:76: 
-<   detected recursive call of function sum_ptr.
-< [eva] tests/value/recursion.c:76: Warning: 
-<   Using specification of function sum_ptr for recursive calls.
-<   Analysis of function sum_ptr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function sum_ptr
-< [eva:alarm] tests/value/recursion.c:68: Warning: 
-<   function sum_ptr: postcondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:69: Warning: 
-<   function sum_ptr: postcondition got status unknown.
-< [eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
-< [eva:recursion] tests/value/recursion.c:89: 
-<   detected recursive call of function factorial_ptr.
-< [eva] tests/value/recursion.c:89: Warning: 
-<   Using specification of function factorial_ptr for recursive calls.
-<   Analysis of function factorial_ptr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function factorial_ptr
-< [eva:alarm] tests/value/recursion.c:90: Warning: 
-<   accessing uninitialized left-value. assert \initialized(&res);
-< [eva] tests/value/recursion.c:358: Frama_C_show_each_120: [0..4294967295]
-< [eva:recursion] tests/value/recursion.c:101: 
-<   detected recursive call of function syracuse_ptr.
-< [eva] tests/value/recursion.c:101: Warning: 
-<   Using specification of function syracuse_ptr for recursive calls.
-<   Analysis of function syracuse_ptr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function syracuse_ptr
-< [eva:alarm] tests/value/recursion.c:102: Warning: 
-<   accessing uninitialized left-value. assert \initialized(&prev_res);
-< [eva] tests/value/recursion.c:361: Frama_C_show_each_1: [0..4294967294]
-< [eva:recursion] tests/value/recursion.c:117: 
-<   detected recursive call of function fibonacci_ptr.
-< [eva] tests/value/recursion.c:117: Warning: 
-<   Using specification of function fibonacci_ptr for recursive calls.
-<   Analysis of function fibonacci_ptr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function fibonacci_ptr
-< [eva:recursion] tests/value/recursion.c:119: 
-<   detected recursive call of function fibonacci_ptr.
-< [eva] tests/value/recursion.c:119: Warning: 
-<   Using specification of function fibonacci_ptr for recursive calls.
-<   Analysis of function fibonacci_ptr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva:alarm] tests/value/recursion.c:120: Warning: 
-<   accessing uninitialized left-value. assert \initialized(&x);
-< [eva:alarm] tests/value/recursion.c:120: Warning: 
-<   accessing uninitialized left-value. assert \initialized(&y);
-< [eva] tests/value/recursion.c:364: Frama_C_show_each_89: [0..4294967295]
-< [eva:recursion] tests/value/recursion.c:137: 
-<   detected recursive call of function sum_and_fact.
-< [eva] tests/value/recursion.c:137: Warning: 
-<   Using specification of function sum_and_fact for recursive calls.
-<   Analysis of function sum_and_fact is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function sum_and_fact
-< [eva:alarm] tests/value/recursion.c:128: Warning: 
-<   function sum_and_fact: postcondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:129: Warning: 
-<   function sum_and_fact: postcondition got status unknown.
-< [eva] tests/value/recursion.c:368: 
-<   Frama_C_show_each_36_40320: {36}, [0..4294967288],0%8
-< [eva:recursion] tests/value/recursion.c:161: 
-<   detected recursive call of function odd.
-< [eva] tests/value/recursion.c:161: Warning: 
-<   Using specification of function odd for recursive calls.
-<   Analysis of function odd is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function odd
-< [eva:alarm] tests/value/recursion.c:149: Warning: 
-<   function odd: postcondition got status unknown.
-< [eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
-< [eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
-< [eva:recursion] tests/value/recursion.c:183: 
-<   detected recursive call of function odd_ptr.
-< [eva] tests/value/recursion.c:183: Warning: 
-<   Using specification of function odd_ptr for recursive calls.
-<   Analysis of function odd_ptr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function odd_ptr
-< [eva:alarm] tests/value/recursion.c:167: Warning: 
-<   function odd_ptr: postcondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:184: Warning: 
-<   accessing uninitialized left-value. assert \initialized(&y);
-< [eva:alarm] tests/value/recursion.c:179: Warning: 
-<   function even_ptr: postcondition got status unknown.
-< [eva:recursion] tests/value/recursion.c:171: 
-<   detected recursive call of function even_ptr.
-< [eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
-< [eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
-< [eva] using specification for function Frama_C_interval
-< [eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
-< [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
-< [eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [0..4294967295]
-< [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [0..4294967295]
-< [eva:alarm] tests/value/recursion.c:222: Warning: 
-<   function fill_array: precondition got status invalid.
-< [eva:alarm] tests/value/recursion.c:226: Warning: 
-<   function fill_array: precondition got status unknown.
-< [eva:recursion] tests/value/recursion.c:200: 
-<   detected recursive call of function fill_array.
-< [eva] tests/value/recursion.c:200: Warning: 
-<   Using specification of function fill_array for recursive calls.
-<   Analysis of function fill_array is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function fill_array
-< [eva:alarm] tests/value/recursion.c:200: Warning: 
-<   function fill_array: precondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:194: Warning: 
-<   function fill_array: postcondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:228: Warning: 
-<   function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
-< [eva:recursion] tests/value/recursion.c:214: 
-<   detected recursive call of function binary_search.
-< [eva] tests/value/recursion.c:214: Warning: 
-<   Using specification of function binary_search for recursive calls.
-<   Analysis of function binary_search is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function binary_search
-< [eva:recursion] tests/value/recursion.c:216: 
-<   detected recursive call of function binary_search.
-< [eva] tests/value/recursion.c:216: Warning: 
-<   Using specification of function binary_search for recursive calls.
-<   Analysis of function binary_search is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] tests/value/recursion.c:229: 
-<   Frama_C_show_each_3: [-2147483648..2147483647]
-< [eva] tests/value/recursion.c:231: 
-<   Frama_C_show_each_12: [-2147483648..2147483647]
-< [eva] tests/value/recursion.c:233: 
-<   Frama_C_show_each_minus1: [-2147483648..2147483647]
-< [eva] tests/value/recursion.c:238: 
-<   Frama_C_show_each_7_11: [-2147483648..2147483647]
-< [eva] tests/value/recursion.c:241: 
-<   Frama_C_show_each_minus_1_15: [-2147483648..2147483647]
-< [eva:recursion] tests/value/recursion.c:252: 
-<   detected recursive call of function alarm.
-< [eva] tests/value/recursion.c:252: Warning: 
-<   Using specification of function alarm for recursive calls.
-<   Analysis of function alarm is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function alarm
-< [eva:alarm] tests/value/recursion.c:247: Warning: 
-<   function alarm: postcondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:252: Warning: 
-<   signed overflow. assert i * tmp ≤ 2147483647;
-<                    (tmp from alarm(i - 1))
-< [eva] tests/value/recursion.c:406: 
-<   Frama_C_show_each_unreachable: [20..2147483640],0%20
-< [eva:recursion] tests/value/recursion.c:261: 
-<   detected recursive call of function precond.
-< [eva] tests/value/recursion.c:261: Warning: 
-<   Using specification of function precond for recursive calls.
-<   Analysis of function precond is thus incomplete and its soundness
-<   relies on the written specification.
-< [inout] Warning: no assigns clauses for function precond.
-<   Results will be imprecise.
-< [eva] using specification for function precond
-< [eva] tests/value/recursion.c:261: Warning: 
-<   Cannot handle empty assigns clause. Assuming assigns \nothing: be aware this is probably incorrect.
-< [eva:recursion] tests/value/recursion.c:276: 
-<   detected recursive call of function escaping_local.
-< [eva] tests/value/recursion.c:276: Warning: 
-<   Using specification of function escaping_local for recursive calls.
-<   Analysis of function escaping_local is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function escaping_local
-< [eva:alarm] tests/value/recursion.c:278: Warning: 
-<   out of bounds write. assert \valid(p);
-< [eva] tests/value/recursion.c:279: Frama_C_show_each_1: {5}
-< [eva:locals-escaping] tests/value/recursion.c:277: Warning: 
-<   locals {x} escaping the scope of a block of escaping_local through p
-< [eva:recursion] tests/value/recursion.c:291: 
-<   detected recursive call of function escaping_formal.
-< [eva] tests/value/recursion.c:291: Warning: 
-<   Using specification of function escaping_formal for recursive calls.
-<   Analysis of function escaping_formal is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function escaping_formal
-< [eva:alarm] tests/value/recursion.c:293: Warning: 
-<   out of bounds write. assert \valid(p);
-< [eva] tests/value/recursion.c:294: Frama_C_show_each_1: {5}
-< [eva:locals-escaping] tests/value/recursion.c:411: Warning: 
-<   locals {x} escaping the scope of escaping_formal through p
-< [eva:recursion] tests/value/recursion.c:307: 
-<   detected recursive call of function escaping_stack.
-< [eva] tests/value/recursion.c:307: Warning: 
-<   Using specification of function escaping_stack for recursive calls.
-<   Analysis of function escaping_stack is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function escaping_stack
-< [eva:alarm] tests/value/recursion.c:309: Warning: 
-<   out of bounds write. assert \valid(p);
-< [eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {5}
-< [eva:locals-escaping] tests/value/recursion.c:308: Warning: 
-<   locals {x} escaping the scope of a block of escaping_stack through p
-< [eva:recursion] tests/value/recursion.c:323: 
-<   detected recursive call of function decr.
-< [eva] tests/value/recursion.c:323: Warning: 
-<   Using specification of function decr for recursive calls.
-<   Analysis of function decr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function decr
-< [eva] done for function main
-< [eva] ====== VALUES COMPUTED ======
-< [eva:final-states] Values at end of function alarm:
-<   res ∈ [10..2147483647]
-<   __retres ∈ [10..2147483647]
-< [eva:final-states] Values at end of function decr:
-<   
-< [eva:final-states] Values at end of function bug_memexec:
-<   
-< [eva:final-states] Values at end of function escaping_formal:
-<   p ∈ {{ NULL + [--..--] ; &x }}
-<   x ∈ [--..--]
-< [eva:final-states] Values at end of function escaping_local:
-<   p ∈ [--..--] or ESCAPINGADDR
-< [eva:final-states] Values at end of function escaping_stack:
-<   p ∈
-<    {{ garbled mix of &{a}
-<     (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
-<   a ∈ [--..--]
-< [eva:final-states] Values at end of function even:
-<   __retres ∈ UNINITIALIZED
-<   __retres ∈ {0; 1}
-< [eva:final-states] Values at end of function even_ptr:
-<   x ∈ [--..--]
-<   b ∈ {0; 1}
-< [eva:final-states] Values at end of function factorial:
-<   res ∈ [--..--]
-<   __retres ∈ [--..--]
-< [eva:final-states] Values at end of function factorial_ptr:
-<   y ∈ [--..--]
-< [eva:final-states] Values at end of function fill_array:
-<   array[0] ∈ {0}
-<        [1..10] ∈ [--..--]
-<        [11..15] ∈ [--..--] or UNINITIALIZED
-< [eva:final-states] Values at end of function five:
-<   __retres ∈ {5}
-< [eva:final-states] Values at end of function odd:
-<   __retres ∈ {0; 1}
-<   __retres ∈ UNINITIALIZED
-< [eva:final-states] Values at end of function odd_ptr:
-<   y ∈ [--..--]
-<   a ∈ [--..--]
-< [eva:final-states] Values at end of function precond:
-< Cannot filter: dumping raw memory (including unchanged variables)
-<   Frama_C_entropy_source ∈ [--..--]
-<   nondet ∈ [--..--]
-<   x ∈ {1}
-<   y ∈ {-6}
-<   p ∈ {0}
-<   a ∈ {0}
-<   b ∈ {0}
-<   x ∈ [10..20]
-<   y ∈ [10..2147483647]
-<   tmp ∈ [3..11]
-<   tmp_0 ∈ [10..20]
-<   tmp_1 ∈ [10..2147483647]
-< [eva:final-states] Values at end of function sum:
-<   res ∈ [6..91]
-<   __retres ∈ [6..91]
-< [eva:final-states] Values at end of function sum_and_fact:
-<   x ∈ {36}
-<   __retres ∈ [0..4294967288],0%8
-< [eva:final-states] Values at end of function sum_ptr:
-<   y ∈ [6..91]
-< [eva:final-states] Values at end of function syracuse:
-<   __retres ∈ [0..4294967294]
-< [eva:final-states] Values at end of function syracuse_ptr:
-<   y ∈ [0..4294967294]
-< [eva:final-states] Values at end of function binary_search:
-<   mid ∈ {7}
-<   __retres ∈ [--..--]
-< [eva:final-states] Values at end of function fibonacci:
-<   __retres ∈ [--..--]
-< [eva:final-states] Values at end of function fibonacci_ptr:
-<   y ∈ [--..--]
-< [eva:final-states] Values at end of function test_array:
-<   Frama_C_entropy_source ∈ [--..--]
-<   array[0] ∈ {0}
-<        [1..9] ∈ [--..--]
-<        [10] ∈ {10}
-<        [11..15] ∈ [--..--]
-<   i ∈ [--..--]
-<   j ∈ [7..18]
-<   end ∈ {10; 11; 12; 13; 14; 15; 16}
-< [eva:final-states] Values at end of function main:
-< Cannot filter: dumping raw memory (including unchanged variables)
-<   Frama_C_entropy_source ∈ [--..--]
-<   nondet ∈ [--..--]
-<   p ∈
-<    {{ garbled mix of &{a}
-<     (origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR
-<   a ∈ [--..--]
-<   b ∈ {0}
-<   x ∈ [10..20]
-<   y ∈ [10..2147483647]
-<   tmp ∈ [3..11]
-<   tmp_0 ∈ [10..20]
-<   tmp_1 ∈ [10..2147483647]
-< [from] Computing for function alarm
-< [from] Computing for function alarm <-alarm
-< [from] Done for function alarm
-< [from] Done for function alarm
-< [from] Computing for function decr
-< [from] Computing for function decr <-decr
-< [from] Done for function decr
-< [from] Done for function decr
-< [from] Computing for function bug_memexec
-< [from] Done for function bug_memexec
-< [from] Computing for function escaping_formal
-< [from] Computing for function escaping_formal <-escaping_formal
-< [from] Done for function escaping_formal
-< [from] Done for function escaping_formal
-< [from] Computing for function escaping_local
-< [from] Computing for function escaping_local <-escaping_local
-< [from] Done for function escaping_local
-< [from] Done for function escaping_local
-< [from] Computing for function escaping_stack
-< [from] Computing for function escaping_stack <-escaping_stack
-< [from] Done for function escaping_stack
-< [from] Done for function escaping_stack
-< [from] Computing for function even
-< [from] Computing for function odd <-even
-< [from] Computing for function even <-odd <-even
-< [from] Done for function even
-< [from] Done for function odd
-< [from] Done for function even
-< [from] Computing for function even_ptr
-< [from] Computing for function odd_ptr <-even_ptr
-< [from] Computing for function even_ptr <-odd_ptr <-even_ptr
-< [from] Done for function even_ptr
-< [from] Done for function odd_ptr
-< [from] Done for function even_ptr
-< [from] Computing for function factorial
-< [from] Computing for function factorial <-factorial
-< [from] Done for function factorial
-< [from] Done for function factorial
-< [from] Computing for function factorial_ptr
-< [from] Computing for function factorial_ptr <-factorial_ptr
-< [from] Done for function factorial_ptr
-< [from] Done for function factorial_ptr
-< [from] Computing for function fill_array
-< [from] Computing for function fill_array <-fill_array
-< [from] Done for function fill_array
-< [from] Done for function fill_array
-< [from] Computing for function five
-< [from] Computing for function five <-five
-< [from] Done for function five
-< [from] Done for function five
-< [from] Computing for function precond
-< [from] Computing for function precond <-precond
-< [from] Done for function precond
-< [from] Done for function precond
-< [from] Computing for function sum
-< [from] Computing for function sum <-sum
-< [from] Done for function sum
-< [from] Done for function sum
-< [from] Computing for function sum_and_fact
-< [from] Computing for function sum_and_fact <-sum_and_fact
-< [from] Done for function sum_and_fact
-< [from] Done for function sum_and_fact
-< [from] Computing for function sum_ptr
-< [from] Computing for function sum_ptr <-sum_ptr
-< [from] Done for function sum_ptr
-< [from] Done for function sum_ptr
-< [from] Computing for function syracuse
-< [from] Computing for function syracuse <-syracuse
-< [from] Done for function syracuse
-< [from] Done for function syracuse
-< [from] Computing for function syracuse_ptr
-< [from] Computing for function syracuse_ptr <-syracuse_ptr
-< [from] Done for function syracuse_ptr
-< [from] Done for function syracuse_ptr
-< [from] Computing for function binary_search
-< [from] Computing for function binary_search <-binary_search
-< [from] Done for function binary_search
-< [from] Done for function binary_search
-< [from] Computing for function fibonacci
-< [from] Computing for function fibonacci <-fibonacci
-< [from] Done for function fibonacci
-< [from] Done for function fibonacci
-< [from] Computing for function fibonacci_ptr
-< [from] Computing for function fibonacci_ptr <-fibonacci_ptr
-< [from] Done for function fibonacci_ptr
-< [from] Done for function fibonacci_ptr
-< [from] Computing for function test_array
-< [from] Computing for function Frama_C_interval <-test_array
-< [from] Done for function Frama_C_interval
-< [from] Done for function test_array
-< [from] Computing for function main
-< [from] Done for function main
-< [from] ====== DEPENDENCIES COMPUTED ======
-<   These dependencies hold at termination for the executions that terminate:
-< [from] Function Frama_C_interval:
-<   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-<   \result FROM Frama_C_entropy_source; min; max
-< [from] Function alarm:
-<   res FROM i
-<   tmp FROM i
-<   __retres FROM i
-<   \result FROM i
-< [from] Function decr:
-<   NO EFFECTS
-< [from] Function bug_memexec:
-<   NO EFFECTS
-< [from] Function escaping_formal:
-<   p FROM count
-<   x FROM nondet; count (and SELF)
-< [from] Function escaping_local:
-<   p FROM count
-< [from] Function escaping_stack:
-<   p FROM count; q
-<   a FROM nondet; count; q (and SELF)
-< [from] Function even:
-<   __retres FROM n
-<   __retres FROM n
-<   \result FROM n
-< [from] Function even_ptr:
-<   x FROM n; result (and SELF)
-<   a FROM n (and SELF)
-<   b FROM n; result (and SELF)
-< [from] Function factorial:
-<   res FROM i
-<   tmp FROM i
-<   __retres FROM i
-<   \result FROM i
-< [from] Function factorial_ptr:
-<   y FROM p_0; result; x
-< [from] Function fill_array:
-<   array{[0]; [10]} FROM data; start; end (and SELF)
-< [from] Function five:
-<   __retres FROM nondet
-<   \result FROM nondet
-< [from] Function odd:
-<   __retres FROM n
-<   \result FROM n
-< [from] Function odd_ptr:
-<   y FROM n; result (and SELF)
-<   a FROM n; result (and SELF)
-< [from] Function precond:
-<   y FROM x
-< [from] Function sum:
-<   res FROM i
-<   tmp FROM i
-<   __retres FROM i
-<   \result FROM i
-< [from] Function sum_and_fact:
-<   x FROM i; sum_0
-<   __retres FROM i
-<   \result FROM i
-< [from] Function sum_ptr:
-<   y FROM p_0; result; x
-< [from] Function syracuse:
-<   __retres FROM i
-<   \result FROM i
-< [from] Function syracuse_ptr:
-<   y FROM p_0; result; x
-< [from] Function binary_search:
-<   mid FROM start; end
-<   __retres FROM data; toFind; start; end; array[7]
-<   \result FROM data; toFind; start; end; array[7]
-< [from] Function fibonacci:
-<   __retres FROM n
-<   \result FROM n
-< [from] Function fibonacci_ptr:
-<   y FROM p_0; result; x
-< [from] Function test_array:
-<   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-< [from] Function main:
-<   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-<   p FROM \nothing
-< [from] ====== END OF DEPENDENCIES ======
-< [inout] Out (internal) for function alarm:
-<     res; tmp; __retres
-< [inout] Inputs for function alarm:
-<     i; res; tmp; __retres
-< [inout] Out (internal) for function decr:
-<     x
-< [inout] Inputs for function decr:
-<     nondet; i
-< [inout] Out (internal) for function bug_memexec:
-<     \nothing
-< [inout] Inputs for function bug_memexec:
-<     nondet
-< [inout] Out (internal) for function escaping_formal:
-<     p; x
-< [inout] Inputs for function escaping_formal:
-<     nondet; p; count; x
-< [inout] Out (internal) for function escaping_local:
-<     p; x
-< [inout] Inputs for function escaping_local:
-<     nondet; p; count
-< [inout] Out (internal) for function escaping_stack:
-<     p; x; a
-< [inout] Inputs for function escaping_stack:
-<     nondet; p; count; q
-< [inout] Out (internal) for function even:
-<     tmp; tmp; __retres; __retres
-< [inout] Inputs for function even:
-<     n; tmp; n; tmp; __retres; __retres
-< [inout] Out (internal) for function even_ptr:
-<     x; y; b
-< [inout] Inputs for function even_ptr:
-<     n; result; x; n; result; y
-< [inout] Out (internal) for function factorial:
-<     res; tmp; __retres
-< [inout] Inputs for function factorial:
-<     i; res; tmp; __retres
-< [inout] Out (internal) for function factorial_ptr:
-<     arg; y
-< [inout] Inputs for function factorial_ptr:
-<     p_0; result; res; x
-< [inout] Out (internal) for function fill_array:
-<     array[0..15]
-< [inout] Inputs for function fill_array:
-<     data; start; end
-< [inout] Out (internal) for function five:
-<     tmp; __retres
-< [inout] Inputs for function five:
-<     nondet; tmp; __retres
-< [inout] Out (internal) for function odd:
-<     tmp; tmp; __retres; __retres
-< [inout] Inputs for function odd:
-<     n; tmp; n; tmp; __retres; __retres
-< [inout] Out (internal) for function odd_ptr:
-<     x; y; a
-< [inout] Inputs for function odd_ptr:
-<     n; result; x; n; result; y
-< [inout] Out (internal) for function precond:
-<     ANYTHING(origin:Unknown)
-< [inout] Inputs for function precond:
-<     nondet; x
-< [inout] Out (internal) for function sum:
-<     res; tmp; __retres
-< [inout] Inputs for function sum:
-<     i; res; tmp; __retres
-< [inout] Out (internal) for function sum_and_fact:
-<     fact; tmp_0; x; __retres
-< [inout] Inputs for function sum_and_fact:
-<     i; sum_0; tmp; fact; tmp_0; __retres
-< [inout] Out (internal) for function sum_ptr:
-<     arg; y
-< [inout] Inputs for function sum_ptr:
-<     p_0; result; res; x
-< [inout] Out (internal) for function syracuse:
-<     prev; __retres
-< [inout] Inputs for function syracuse:
-<     n; i; prev; __retres
-< [inout] Out (internal) for function syracuse_ptr:
-<     prev_arg; y
-< [inout] Inputs for function syracuse_ptr:
-<     n; p_0; result; prev_res; x
-< [inout] Out (internal) for function binary_search:
-<     mid; tmp; tmp_0; __retres
-< [inout] Inputs for function binary_search:
-<     data; toFind; start; end; mid; tmp; tmp_0; array[7]; __retres
-< [inout] Out (internal) for function fibonacci:
-<     x; y; __retres
-< [inout] Inputs for function fibonacci:
-<     n; x; y; __retres
-< [inout] Out (internal) for function fibonacci_ptr:
-<     a; y
-< [inout] Inputs for function fibonacci_ptr:
-<     p_0; result; x; y; a; x
-< [inout] Out (internal) for function test_array:
-<     Frama_C_entropy_source; array[0..15]; i; j; end
-< [inout] Inputs for function test_array:
-<     Frama_C_entropy_source; nondet
-< [inout] Out (internal) for function main:
-<     ANYTHING(origin:Unknown)
-< [inout] Inputs for function main:
-<     Frama_C_entropy_source; nondet; p
----
-> [eva] tests/value/recursion.c:18: User Error: 
->   The binding to APRON domains does not support recursive calls.
-> [kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle_apron/recursion.1.res.oracle b/tests/value/oracle_apron/recursion.1.res.oracle
deleted file mode 100644
index 7556d61ac85a09c7c94d6176127ef66655521b91..0000000000000000000000000000000000000000
--- a/tests/value/oracle_apron/recursion.1.res.oracle
+++ /dev/null
@@ -1,510 +0,0 @@
-10,514c10,12
-< [eva] tests/value/recursion.c:18: Warning: 
-<   Using specification of function five for recursive calls of depth 20.
-<   Analysis of function five is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function five
-< [eva:alarm] tests/value/recursion.c:15: Warning: 
-<   function five: postcondition got status unknown.
-< [eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
-< [eva:recursion] tests/value/recursion.c:28: 
-<   detected recursive call of function sum.
-< [eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
-< [eva:recursion] tests/value/recursion.c:37: 
-<   detected recursive call of function factorial.
-< [eva] tests/value/recursion.c:346: Frama_C_show_each_120: {120}
-< [eva:recursion] tests/value/recursion.c:46: 
-<   detected recursive call of function syracuse.
-< [eva] tests/value/recursion.c:348: Frama_C_show_each_1: {1}
-< [eva:recursion] tests/value/recursion.c:59: 
-<   detected recursive call of function fibonacci.
-< [eva:recursion] tests/value/recursion.c:60: 
-<   detected recursive call of function fibonacci.
-< [eva] tests/value/recursion.c:350: Frama_C_show_each_89: {89}
-< [eva:recursion] tests/value/recursion.c:76: 
-<   detected recursive call of function sum_ptr.
-< [eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
-< [eva:recursion] tests/value/recursion.c:89: 
-<   detected recursive call of function factorial_ptr.
-< [eva] tests/value/recursion.c:358: Frama_C_show_each_120: {120}
-< [eva:recursion] tests/value/recursion.c:101: 
-<   detected recursive call of function syracuse_ptr.
-< [eva] tests/value/recursion.c:361: Frama_C_show_each_1: {1}
-< [eva:recursion] tests/value/recursion.c:117: 
-<   detected recursive call of function fibonacci_ptr.
-< [eva:recursion] tests/value/recursion.c:119: 
-<   detected recursive call of function fibonacci_ptr.
-< [eva] tests/value/recursion.c:364: Frama_C_show_each_89: {89}
-< [eva:recursion] tests/value/recursion.c:137: 
-<   detected recursive call of function sum_and_fact.
-< [eva] tests/value/recursion.c:368: Frama_C_show_each_36_40320: {36}, {40320}
-< [eva:recursion] tests/value/recursion.c:161: 
-<   detected recursive call of function odd.
-< [eva:recursion] tests/value/recursion.c:152: 
-<   detected recursive call of function even.
-< [eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
-< [eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
-< [eva:recursion] tests/value/recursion.c:183: 
-<   detected recursive call of function odd_ptr.
-< [eva:recursion] tests/value/recursion.c:171: 
-<   detected recursive call of function even_ptr.
-< [eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
-< [eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
-< [eva] using specification for function Frama_C_interval
-< [eva:alarm] tests/value/recursion.c:24: Warning: 
-<   function sum: postcondition got status unknown.
-< [eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
-< [eva:alarm] tests/value/recursion.c:69: Warning: 
-<   function sum_ptr: postcondition got status unknown.
-< [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
-< [eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [2..89]
-< [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [2..89]
-< [eva:alarm] tests/value/recursion.c:222: Warning: 
-<   function fill_array: precondition got status invalid.
-< [eva:alarm] tests/value/recursion.c:226: Warning: 
-<   function fill_array: precondition got status unknown.
-< [eva:recursion] tests/value/recursion.c:200: 
-<   detected recursive call of function fill_array.
-< [eva:alarm] tests/value/recursion.c:200: Warning: 
-<   function fill_array: precondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:199: Warning: 
-<   out of bounds write. assert \valid(data + start);
-< [kernel] tests/value/recursion.c:199: Warning: 
-<   all target addresses were invalid. This path is assumed to be dead.
-< [eva:alarm] tests/value/recursion.c:194: Warning: 
-<   function fill_array: postcondition got status unknown.
-< [eva:alarm] tests/value/recursion.c:228: Warning: 
-<   function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
-< [eva:recursion] tests/value/recursion.c:214: 
-<   detected recursive call of function binary_search.
-< [eva] tests/value/recursion.c:229: Frama_C_show_each_3: {3}
-< [eva:recursion] tests/value/recursion.c:216: 
-<   detected recursive call of function binary_search.
-< [eva] tests/value/recursion.c:231: Frama_C_show_each_12: {12}
-< [eva] tests/value/recursion.c:233: Frama_C_show_each_minus1: {-1}
-< [eva] tests/value/recursion.c:238: Frama_C_show_each_7_11: {7; 8; 9; 10; 11}
-< [eva] tests/value/recursion.c:241: Frama_C_show_each_minus_1_15: [-1..15]
-< [eva:recursion] tests/value/recursion.c:252: 
-<   detected recursive call of function alarm.
-< [eva:alarm] tests/value/recursion.c:252: Warning: 
-<   signed overflow. assert i * tmp ≤ 2147483647;
-<                    (tmp from alarm(i - 1))
-< [eva:recursion] tests/value/recursion.c:261: 
-<   detected recursive call of function precond.
-< [eva:alarm] tests/value/recursion.c:261: Warning: 
-<   function precond: precondition got status invalid.
-< [eva:recursion] tests/value/recursion.c:276: 
-<   detected recursive call of function escaping_local.
-< [eva] tests/value/recursion.c:279: Frama_C_show_each_1: {1}
-< [eva:locals-escaping] tests/value/recursion.c:277: Warning: 
-<   locals {x} escaping the scope of a block of escaping_local through p
-< [eva:alarm] tests/value/recursion.c:278: Warning: 
-<   accessing left-value that contains escaping addresses.
-<   assert ¬\dangling(&p);
-< [kernel] tests/value/recursion.c:278: Warning: 
-<   all target addresses were invalid. This path is assumed to be dead.
-< [eva:recursion] tests/value/recursion.c:291: 
-<   detected recursive call of function escaping_formal.
-< [eva] tests/value/recursion.c:294: Frama_C_show_each_1: {1}
-< [eva:locals-escaping] tests/value/recursion.c:291: Warning: 
-<   locals {x} escaping the scope of escaping_formal through p
-< [eva:alarm] tests/value/recursion.c:293: Warning: 
-<   accessing left-value that contains escaping addresses.
-<   assert ¬\dangling(&p);
-< [kernel] tests/value/recursion.c:293: Warning: 
-<   all target addresses were invalid. This path is assumed to be dead.
-< [eva:recursion] tests/value/recursion.c:307: 
-<   detected recursive call of function escaping_stack.
-< [eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {1}
-< [eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {2}
-< [eva:locals-escaping] tests/value/recursion.c:308: Warning: 
-<   locals {x} escaping the scope of a block of escaping_stack through p
-< [eva:alarm] tests/value/recursion.c:309: Warning: 
-<   accessing left-value that contains escaping addresses.
-<   assert ¬\dangling(&p);
-< [kernel] tests/value/recursion.c:309: Warning: 
-<   all target addresses were invalid. This path is assumed to be dead.
-< [eva:recursion] tests/value/recursion.c:323: 
-<   detected recursive call of function decr.
-< [eva] tests/value/recursion.c:323: Warning: 
-<   Using specification of function decr for recursive calls of depth 20.
-<   Analysis of function decr is thus incomplete and its soundness
-<   relies on the written specification.
-< [eva] using specification for function decr
-< [eva] done for function main
-< [eva] ====== VALUES COMPUTED ======
-< [eva:final-states] Values at end of function alarm:
-<   res ∈ [2..2147483647]
-<   __retres ∈ [1..2147483647]
-< [eva:final-states] Values at end of function decr:
-<   
-< [eva:final-states] Values at end of function bug_memexec:
-<   
-< [eva:final-states] Values at end of function escaping_formal:
-<   p ∈ {{ &x ; &\copy<x>[5] }} or ESCAPINGADDR
-<   x ∈ {5; 16}
-< [eva:final-states] Values at end of function escaping_local:
-<   p ∈ {{ &\copy<x>[5] }} or ESCAPINGADDR
-< [eva:final-states] Values at end of function escaping_stack:
-<   p ∈ {{ &\copy<x>[4] }} or ESCAPINGADDR
-< [eva:final-states] Values at end of function even:
-<   __retres ∈ UNINITIALIZED
-<   __retres ∈ {0; 1}
-< [eva:final-states] Values at end of function even_ptr:
-<   x ∈ {0; 1}
-<   b ∈ {0; 1}
-< [eva:final-states] Values at end of function factorial:
-<   res ∈ {2; 6; 24; 120}
-<   __retres ∈ {1; 2; 6; 24; 120}
-< [eva:final-states] Values at end of function factorial_ptr:
-<   y ∈ {91; 120}
-< [eva:final-states] Values at end of function fill_array:
-<   array[0] ∈ {0}
-<        [1] ∈ {1}
-<        [2] ∈ {2}
-<        [3] ∈ {3}
-<        [4] ∈ {4}
-<        [5] ∈ {5}
-<        [6] ∈ {6}
-<        [7] ∈ {7}
-<        [8] ∈ {8}
-<        [9] ∈ {9}
-<        [10] ∈ {10}
-<        [11] ∈ {11} or UNINITIALIZED
-<        [12] ∈ {12} or UNINITIALIZED
-<        [13] ∈ {13} or UNINITIALIZED
-<        [14] ∈ {14} or UNINITIALIZED
-<        [15] ∈ {15} or UNINITIALIZED
-< [eva:final-states] Values at end of function five:
-<   __retres ∈ {5}
-< [eva:final-states] Values at end of function odd:
-<   __retres ∈ {0; 1}
-<   __retres ∈ UNINITIALIZED
-< [eva:final-states] Values at end of function odd_ptr:
-<   y ∈ {0; 1}
-<   a ∈ {0; 1}
-< [eva:final-states] Values at end of function precond:
-<   y ∈ [-100..-6]
-< [eva:final-states] Values at end of function sum:
-<   res ∈ [3..91]
-<   __retres ∈ [1..91]
-< [eva:final-states] Values at end of function sum_and_fact:
-<   x ∈ {11; 36}
-<   __retres ∈ {1; 2; 6; 24; 120; 720; 5040; 40320}
-< [eva:final-states] Values at end of function sum_ptr:
-<   y ∈ [0..91]
-< [eva:final-states] Values at end of function syracuse:
-<   __retres ∈ [1..16]
-< [eva:final-states] Values at end of function syracuse_ptr:
-<   y ∈ {1; 120}
-< [eva:final-states] Values at end of function binary_search:
-<   mid ∈ [3..16]
-<   __retres ∈ [-1..15]
-< [eva:final-states] Values at end of function fibonacci:
-<   __retres ∈ [0..89]
-< [eva:final-states] Values at end of function fibonacci_ptr:
-<   y ∈ [0..89]
-< [eva:final-states] Values at end of function test_array:
-<   Frama_C_entropy_source ∈ [--..--]
-<   array[0] ∈ {0}
-<        [1] ∈ {1}
-<        [2] ∈ {2}
-<        [3] ∈ {3}
-<        [4] ∈ {4}
-<        [5] ∈ {5}
-<        [6] ∈ {6}
-<        [7] ∈ {7}
-<        [8] ∈ {8}
-<        [9] ∈ {9}
-<        [10] ∈ {10}
-<        [11] ∈ {11}
-<        [12] ∈ {12}
-<        [13] ∈ {13}
-<        [14] ∈ {14}
-<        [15] ∈ {15}
-<   i ∈ [-1..15]
-<   j ∈ [7..18]
-<   end ∈ {10; 11; 12; 13; 14; 15}
-< [eva:final-states] Values at end of function main:
-<   Frama_C_entropy_source ∈ [--..--]
-<   p ∈ ESCAPINGADDR
-<   a ∈ {0}
-<   b ∈ {0}
-<   x ∈ [10..20]
-<   y ∈ [3628800..2147483647]
-< [from] Computing for function alarm
-< [from] Computing for function alarm <-alarm
-< [from] Done for function alarm
-< [from] Done for function alarm
-< [from] Computing for function decr
-< [from] Computing for function decr <-decr
-< [from] Done for function decr
-< [from] Done for function decr
-< [from] Computing for function bug_memexec
-< [from] Done for function bug_memexec
-< [from] Computing for function escaping_formal
-< [from] Computing for function escaping_formal <-escaping_formal
-< [from] Done for function escaping_formal
-< [from] Done for function escaping_formal
-< [from] Computing for function escaping_local
-< [from] Computing for function escaping_local <-escaping_local
-< [from] Done for function escaping_local
-< [from] Done for function escaping_local
-< [from] Computing for function escaping_stack
-< [from] Computing for function escaping_stack <-escaping_stack
-< [from] Done for function escaping_stack
-< [from] Done for function escaping_stack
-< [from] Computing for function even
-< [from] Computing for function odd <-even
-< [from] Computing for function even <-odd <-even
-< [from] Done for function even
-< [from] Done for function odd
-< [from] Done for function even
-< [from] Computing for function even_ptr
-< [from] Computing for function odd_ptr <-even_ptr
-< [from] Computing for function even_ptr <-odd_ptr <-even_ptr
-< [from] Done for function even_ptr
-< [from] Done for function odd_ptr
-< [from] Done for function even_ptr
-< [from] Computing for function factorial
-< [from] Computing for function factorial <-factorial
-< [from] Done for function factorial
-< [from] Done for function factorial
-< [from] Computing for function factorial_ptr
-< [from] Computing for function factorial_ptr <-factorial_ptr
-< [from] Done for function factorial_ptr
-< [from] Done for function factorial_ptr
-< [from] Computing for function fill_array
-< [from] Computing for function fill_array <-fill_array
-< [from] Done for function fill_array
-< [from] Done for function fill_array
-< [from] Computing for function five
-< [from] Computing for function five <-five
-< [from] Done for function five
-< [from] Done for function five
-< [from] Computing for function precond
-< [from] Computing for function precond <-precond
-< [from] Done for function precond
-< [from] Done for function precond
-< [from] Computing for function sum
-< [from] Computing for function sum <-sum
-< [from] Done for function sum
-< [from] Done for function sum
-< [from] Computing for function sum_and_fact
-< [from] Computing for function sum_and_fact <-sum_and_fact
-< [from] Done for function sum_and_fact
-< [from] Done for function sum_and_fact
-< [from] Computing for function sum_ptr
-< [from] Computing for function sum_ptr <-sum_ptr
-< [from] Done for function sum_ptr
-< [from] Done for function sum_ptr
-< [from] Computing for function syracuse
-< [from] Computing for function syracuse <-syracuse
-< [from] Done for function syracuse
-< [from] Done for function syracuse
-< [from] Computing for function syracuse_ptr
-< [from] Computing for function syracuse_ptr <-syracuse_ptr
-< [from] Done for function syracuse_ptr
-< [from] Done for function syracuse_ptr
-< [from] Computing for function binary_search
-< [from] Computing for function binary_search <-binary_search
-< [from] Done for function binary_search
-< [from] Done for function binary_search
-< [from] Computing for function fibonacci
-< [from] Computing for function fibonacci <-fibonacci
-< [from] Done for function fibonacci
-< [from] Done for function fibonacci
-< [from] Computing for function fibonacci_ptr
-< [from] Computing for function fibonacci_ptr <-fibonacci_ptr
-< [from] Done for function fibonacci_ptr
-< [from] Done for function fibonacci_ptr
-< [from] Computing for function test_array
-< [from] Computing for function Frama_C_interval <-test_array
-< [from] Done for function Frama_C_interval
-< [from] Done for function test_array
-< [from] Computing for function main
-< [from] Done for function main
-< [from] ====== DEPENDENCIES COMPUTED ======
-<   These dependencies hold at termination for the executions that terminate:
-< [from] Function Frama_C_interval:
-<   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-<   \result FROM Frama_C_entropy_source; min; max
-< [from] Function alarm:
-<   res FROM i
-<   tmp FROM i
-<   __retres FROM i
-<   \result FROM i
-< [from] Function decr:
-<   NO EFFECTS
-< [from] Function bug_memexec:
-<   NO EFFECTS
-< [from] Function escaping_formal:
-<   p FROM count (and SELF)
-<   x FROM nondet; count (and SELF)
-< [from] Function escaping_local:
-<   p FROM count (and SELF)
-< [from] Function escaping_stack:
-<   p FROM count; q (and SELF)
-< [from] Function even:
-<   __retres FROM n (and SELF)
-<   __retres FROM n
-<   \result FROM n
-< [from] Function even_ptr:
-<   x FROM n; result (and SELF)
-<   a FROM n (and SELF)
-<   b FROM n; result (and SELF)
-< [from] Function factorial:
-<   res FROM i
-<   tmp FROM i
-<   __retres FROM i
-<   \result FROM i
-< [from] Function factorial_ptr:
-<   y FROM p_0; result; x (and SELF)
-< [from] Function fill_array:
-<   array[0..15] FROM data; start; end (and SELF)
-< [from] Function five:
-<   __retres FROM nondet
-<   \result FROM nondet
-< [from] Function odd:
-<   __retres FROM n
-<   \result FROM n
-< [from] Function odd_ptr:
-<   y FROM n; result (and SELF)
-<   a FROM n; result (and SELF)
-< [from] Function precond:
-<   y FROM x
-< [from] Function sum:
-<   res FROM i
-<   tmp FROM i
-<   __retres FROM i
-<   \result FROM i
-< [from] Function sum_and_fact:
-<   x FROM i; sum_0 (and SELF)
-<   __retres FROM i
-<   \result FROM i
-< [from] Function sum_ptr:
-<   y FROM p_0; result; x (and SELF)
-< [from] Function syracuse:
-<   __retres FROM n; i
-<   \result FROM n; i
-< [from] Function syracuse_ptr:
-<   y FROM p_0; result; x (and SELF)
-< [from] Function binary_search:
-<   mid FROM start; end
-<   __retres FROM data; toFind; start; end; array[3..15]
-<   \result FROM data; toFind; start; end; array[3..15]
-< [from] Function fibonacci:
-<   __retres FROM n
-<   \result FROM n
-< [from] Function fibonacci_ptr:
-<   y FROM p_0; result; x (and SELF)
-< [from] Function test_array:
-<   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-< [from] Function main:
-<   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-<   p FROM \nothing (and SELF)
-< [from] ====== END OF DEPENDENCIES ======
-< [inout] Out (internal) for function alarm:
-<     res; tmp; __retres
-< [inout] Inputs for function alarm:
-<     i; res; tmp; __retres
-< [inout] Out (internal) for function decr:
-<     x
-< [inout] Inputs for function decr:
-<     nondet; i
-< [inout] Out (internal) for function bug_memexec:
-<     \nothing
-< [inout] Inputs for function bug_memexec:
-<     nondet
-< [inout] Out (internal) for function escaping_formal:
-<     p; x
-< [inout] Inputs for function escaping_formal:
-<     nondet; p; count; x
-< [inout] Out (internal) for function escaping_local:
-<     p; x
-< [inout] Inputs for function escaping_local:
-<     nondet; p; count
-< [inout] Out (internal) for function escaping_stack:
-<     p; x
-< [inout] Inputs for function escaping_stack:
-<     nondet; p; count; q
-< [inout] Out (internal) for function even:
-<     tmp; tmp; __retres; __retres
-< [inout] Inputs for function even:
-<     n; tmp; n; tmp; __retres; __retres
-< [inout] Out (internal) for function even_ptr:
-<     x; y; b
-< [inout] Inputs for function even_ptr:
-<     n; result; x; n; result; y
-< [inout] Out (internal) for function factorial:
-<     res; tmp; __retres
-< [inout] Inputs for function factorial:
-<     i; res; tmp; __retres
-< [inout] Out (internal) for function factorial_ptr:
-<     arg; y
-< [inout] Inputs for function factorial_ptr:
-<     p_0; result; res; x
-< [inout] Out (internal) for function fill_array:
-<     array[0..15]
-< [inout] Inputs for function fill_array:
-<     data; start; end
-< [inout] Out (internal) for function five:
-<     tmp; __retres
-< [inout] Inputs for function five:
-<     nondet; tmp; __retres
-< [inout] Out (internal) for function odd:
-<     tmp; tmp; __retres; __retres
-< [inout] Inputs for function odd:
-<     n; tmp; n; tmp; __retres; __retres
-< [inout] Out (internal) for function odd_ptr:
-<     x; y; a
-< [inout] Inputs for function odd_ptr:
-<     n; result; x; n; result; y
-< [inout] Out (internal) for function precond:
-<     y
-< [inout] Inputs for function precond:
-<     nondet; x
-< [inout] Out (internal) for function sum:
-<     res; tmp; __retres
-< [inout] Inputs for function sum:
-<     i; res; tmp; __retres
-< [inout] Out (internal) for function sum_and_fact:
-<     fact; tmp_0; x; __retres
-< [inout] Inputs for function sum_and_fact:
-<     i; sum_0; tmp; fact; tmp_0; __retres
-< [inout] Out (internal) for function sum_ptr:
-<     arg; y
-< [inout] Inputs for function sum_ptr:
-<     p_0; result; res; x
-< [inout] Out (internal) for function syracuse:
-<     prev; __retres
-< [inout] Inputs for function syracuse:
-<     n; i; prev; __retres
-< [inout] Out (internal) for function syracuse_ptr:
-<     prev_arg; y
-< [inout] Inputs for function syracuse_ptr:
-<     n; p_0; result; prev_res; x
-< [inout] Out (internal) for function binary_search:
-<     mid; tmp; tmp_0; __retres
-< [inout] Inputs for function binary_search:
-<     data; toFind; start; end; mid; tmp; tmp_0; array[3..15]; __retres
-< [inout] Out (internal) for function fibonacci:
-<     x; y; __retres
-< [inout] Inputs for function fibonacci:
-<     n; x; y; __retres
-< [inout] Out (internal) for function fibonacci_ptr:
-<     a; y
-< [inout] Inputs for function fibonacci_ptr:
-<     p_0; result; x; y; a; x
-< [inout] Out (internal) for function test_array:
-<     Frama_C_entropy_source; array[0..15]; i; j; end
-< [inout] Inputs for function test_array:
-<     Frama_C_entropy_source; nondet
-< [inout] Out (internal) for function main:
-<     Frama_C_entropy_source; p; a; b; x; y; tmp; tmp_0; tmp_1; tmp_2
-< [inout] Inputs for function main:
-<     Frama_C_entropy_source; nondet; p
----
-> [eva] tests/value/recursion.c:18: User Error: 
->   The binding to APRON domains does not support recursive calls.
-> [kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle_apron/recursion.2.res.oracle b/tests/value/oracle_apron/recursion.2.res.oracle
deleted file mode 100644
index 61f9a6838a929c95b6fd56661df773f25660b4e3..0000000000000000000000000000000000000000
--- a/tests/value/oracle_apron/recursion.2.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-10,12d9
-< [eva] tests/value/recursion.c:429: Frama_C_show_each_10: {10}
-< [eva] tests/value/recursion.c:434: Frama_C_show_each_36: {36}
-< [eva] using specification for function Frama_C_interval
-14,16c11
-<   Recursive call to sum_nospec without a specification. Try to increase
-<   the -eva-unroll-recursive-calls parameter or write a specification
-<   for function sum_nospec.
----
->   The binding to APRON domains does not support recursive calls.
diff --git a/tests/value/recursion.c b/tests/value/recursion.c
index 1dad1842fcd65526388f6ca3bc2d1a08a340c7d3..7e7a3365b87951e58c0f2b9a88fb4bc2c03efa75 100644
--- a/tests/value/recursion.c
+++ b/tests/value/recursion.c
@@ -1,8 +1,11 @@
+/* run.config_apron
+   DONTRUN: The apron binding does not support recursion.
+*/
 /* run.config*
-  STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 0"
-  STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 20"
-  EXIT: 1
-  STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 5 -main main_fail"
+   STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 0"
+   STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 20"
+   EXIT: 1
+   STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 5 -main main_fail"
 */
 
 #include <__fc_builtin.h>