diff --git a/tests/test_config_equalities b/tests/test_config_equalities
index 45664b6c91351aae50544f999ad2d98142ee818e..ffa23c9d32dac550f13db32f54185a48c1b3772e 100644
--- a/tests/test_config_equalities
+++ b/tests/test_config_equalities
@@ -1,3 +1,7 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+
+# Compare the result with the oracle of the default config.
+FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
+
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/oracle_equalities/CruiseControl.res.oracle b/tests/value/oracle_equalities/CruiseControl.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..977bd6ffca38f631eb8c630e89d3709078392599
--- /dev/null
+++ b/tests/value/oracle_equalities/CruiseControl.res.oracle
@@ -0,0 +1,45 @@
+980c980
+< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
+---
+> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}
+1018c1018
+< [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle{._I0_ThrottleIn; ._O0_ThrottleOut} ∈
+---
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._I0_ThrottleIn ∈
+1019a1020,1021
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._O0_ThrottleOut ∈
+> [-0.0000000000000000 .. 1.9999998807907104*2^127]
+1033c1035
+< [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
+---
+> [-0.0000000000000000 .. 1.9999998807907104*2^127]
+1218c1220
+< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
+---
+> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}
+1230c1232,1236
+< [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._I1_CruiseSpeed; ._I2_VehiculeSpeed; ._O0_Throttle; ._L1_CruiseControl; ._L2_CruiseControl; ._L3_CruiseControl} ∈
+---
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._I1_CruiseSpeed; ._I2_VehiculeSpeed} ∈
+> [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._O0_Throttle ∈
+> [-0.0000000000000000 .. 1.9999998807907104*2^127]
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._L1_CruiseControl; ._L2_CruiseControl; ._L3_CruiseControl} ∈
+1248c1254
+< [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._L4_CruiseControl; ._L13_CruiseControl} ∈
+---
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._L4_CruiseControl ∈
+1249a1256,1257
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._L13_CruiseControl ∈
+> [-0.0000000000000000 .. 1.9999998807907104*2^127]
+1256c1264
+< [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle{._I0_ThrottleIn; ._O0_ThrottleOut} ∈
+---
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._I0_ThrottleIn ∈
+1257a1266,1267
+> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._O0_ThrottleOut ∈
+> [-0.0000000000000000 .. 1.9999998807907104*2^127]
+1271c1281
+< [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
+---
+> [-0.0000000000000000 .. 1.9999998807907104*2^127]
diff --git a/tests/value/oracle_equalities/FP5.res.oracle b/tests/value/oracle_equalities/FP5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/abs.res.oracle b/tests/value/oracle_equalities/abs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/abs_addr.res.oracle b/tests/value/oracle_equalities/abs_addr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/absolute_pointer.res.oracle b/tests/value/oracle_equalities/absolute_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/abstract_struct_1.res.oracle b/tests/value/oracle_equalities/abstract_struct_1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/access_path.res.oracle b/tests/value/oracle_equalities/access_path.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/add_approx.res.oracle b/tests/value/oracle_equalities/add_approx.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/addition.res.oracle b/tests/value/oracle_equalities/addition.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..98c7d2372434290cc2f334cddcb6bc9466e6ac7f
--- /dev/null
+++ b/tests/value/oracle_equalities/addition.res.oracle
@@ -0,0 +1,18 @@
+138,141d137
+< [eva:alarm] tests/value/addition.i:61: Warning:
+< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
+< [eva:alarm] tests/value/addition.i:61: Warning:
+< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
+168c164
+< [scope:rm_asserts] removing 9 assertion(s)
+---
+> [scope:rm_asserts] removing 7 assertion(s)
+407,410d402
+< [eva:alarm] tests/value/addition.i:61: Warning:
+< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
+< [eva:alarm] tests/value/addition.i:61: Warning:
+< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
+433c425
+< [scope:rm_asserts] removing 9 assertion(s)
+---
+> [scope:rm_asserts] removing 7 assertion(s)
diff --git a/tests/value/oracle_equalities/addr.0.res.oracle b/tests/value/oracle_equalities/addr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/addr.1.res.oracle b/tests/value/oracle_equalities/addr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/addr2.res.oracle b/tests/value/oracle_equalities/addr2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/addrofstring.res.oracle b/tests/value/oracle_equalities/addrofstring.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/affect_corrupt.0.res.oracle b/tests/value/oracle_equalities/affect_corrupt.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/affect_corrupt.1.res.oracle b/tests/value/oracle_equalities/affect_corrupt.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ai_annot.res.oracle b/tests/value/oracle_equalities/ai_annot.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/alias.0.res.oracle b/tests/value/oracle_equalities/alias.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c234ab23c2ef7ade7fb11fd8bd401d1a710a0a37
--- /dev/null
+++ b/tests/value/oracle_equalities/alias.0.res.oracle
@@ -0,0 +1,10 @@
+103,104c103,104
+< t ∈ {1; 2; 4}
+< u ∈ {2; 3; 4; 5}
+---
+> t ∈ {4}
+> u ∈ {5}
+110c110
+< t2 ∈ {0; 3; 6}
+---
+> t2 ∈ {6}
diff --git a/tests/value/oracle_equalities/alias.1.res.oracle b/tests/value/oracle_equalities/alias.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..83f51b9015d62efe57f3906b3efd2228b99697ea
--- /dev/null
+++ b/tests/value/oracle_equalities/alias.1.res.oracle
@@ -0,0 +1,18 @@
+85c85
+< z ∈ {0; 1; 2}
+---
+> z ∈ {0; 2}
+87,88c87,88
+< v2 ∈ {-1; 0; 1; 2; 3; 4}
+< PTR1 ∈ {{ &p2{[0], [1], [2]} }}
+---
+> v2 ∈ {0; 1; 2}
+> PTR1 ∈ {{ &p2{[0], [1]} }}
+90c90
+< PTR3 ∈ {{ &p2{[1], [2], [4]} }}
+---
+> PTR3 ∈ {{ &p2{[1], [2]} }}
+110c110
+< t2 FROM p2[0..2]; c
+---
+> t2 FROM p2[0..1]; c
diff --git a/tests/value/oracle_equalities/alias.2.res.oracle b/tests/value/oracle_equalities/alias.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..686417eb7ea8aabf15bf58576ecd3afcd58780e1
--- /dev/null
+++ b/tests/value/oracle_equalities/alias.2.res.oracle
@@ -0,0 +1,4 @@
+76c76
+< z ∈ {-5; -4; -3; -2; -1; 0; 1; 1000}
+---
+> z ∈ {-2; -1; 0; 1000}
diff --git a/tests/value/oracle_equalities/alias.3.res.oracle b/tests/value/oracle_equalities/alias.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e14f1380123bfd42bbd395f88c728c05558d44b3
--- /dev/null
+++ b/tests/value/oracle_equalities/alias.3.res.oracle
@@ -0,0 +1,4 @@
+67c67
+< z ∈ {0; 1; 2}
+---
+> z ∈ {0; 2}
diff --git a/tests/value/oracle_equalities/alias.4.res.oracle b/tests/value/oracle_equalities/alias.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f45634e31c8c1322a448c5a229319212361daf9f
--- /dev/null
+++ b/tests/value/oracle_equalities/alias.4.res.oracle
@@ -0,0 +1,4 @@
+81c81
+< y ∈ {0; 3; 77}
+---
+> y ∈ {77}
diff --git a/tests/value/oracle_equalities/alias.5.res.oracle b/tests/value/oracle_equalities/alias.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e34839d5f87a29da21a6edffc596a85c576e8f31
--- /dev/null
+++ b/tests/value/oracle_equalities/alias.5.res.oracle
@@ -0,0 +1,6 @@
+59a60
+> [eva] tests/value/alias.i:260: starting to merge loop iterations
+170c171
+< y ∈ {0; 3; 77}
+---
+> y ∈ {77}
diff --git a/tests/value/oracle_equalities/alias.6.res.oracle b/tests/value/oracle_equalities/alias.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a7dfd3031756c0781ca8579ae7e21c2b0a65e1c0
--- /dev/null
+++ b/tests/value/oracle_equalities/alias.6.res.oracle
@@ -0,0 +1,4 @@
+86c86
+< x ∈ {0; 4; 33}
+---
+> x ∈ {33}
diff --git a/tests/value/oracle_equalities/align.res.oracle b/tests/value/oracle_equalities/align.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/align_char_array.res.oracle b/tests/value/oracle_equalities/align_char_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/annot.res.oracle b/tests/value/oracle_equalities/annot.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/annot_valid.res.oracle b/tests/value/oracle_equalities/annot_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/anonymous_field.res.oracle b/tests/value/oracle_equalities/anonymous_field.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/any_int.res.oracle b/tests/value/oracle_equalities/any_int.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/arch.res.oracle b/tests/value/oracle_equalities/arch.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/arg_array.res.oracle b/tests/value/oracle_equalities/arg_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/arith_pointer.res.oracle b/tests/value/oracle_equalities/arith_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_access.res.oracle b/tests/value/oracle_equalities/array_access.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_array.0.res.oracle b/tests/value/oracle_equalities/array_array.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_array.1.res.oracle b/tests/value/oracle_equalities/array_array.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_array.2.res.oracle b/tests/value/oracle_equalities/array_array.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_bounds.0.res.oracle b/tests/value/oracle_equalities/array_bounds.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_bounds.1.res.oracle b/tests/value/oracle_equalities/array_bounds.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_degenerating_loop.res.oracle b/tests/value/oracle_equalities/array_degenerating_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_initializer.res.oracle b/tests/value/oracle_equalities/array_initializer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_loop.res.oracle b/tests/value/oracle_equalities/array_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_overlap.res.oracle b/tests/value/oracle_equalities/array_overlap.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_ptr.res.oracle b/tests/value/oracle_equalities/array_ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_zero_length.0.res.oracle b/tests/value/oracle_equalities/array_zero_length.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_zero_length.1.res.oracle b/tests/value/oracle_equalities/array_zero_length.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/array_zero_length.2.res.oracle b/tests/value/oracle_equalities/array_zero_length.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/asm_contracts.res.oracle b/tests/value/oracle_equalities/asm_contracts.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/assert_ptr.res.oracle b/tests/value/oracle_equalities/assert_ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/assign-leaf-indirect.res.oracle b/tests/value/oracle_equalities/assign-leaf-indirect.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/assigns.res.oracle b/tests/value/oracle_equalities/assigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/assigns_from.res.oracle b/tests/value/oracle_equalities/assigns_from.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/assigns_from_direct.res.oracle b/tests/value/oracle_equalities/assigns_from_direct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/attribute-aligned.res.oracle b/tests/value/oracle_equalities/attribute-aligned.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/audit.res.oracle b/tests/value/oracle_equalities/audit.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9ff41db248872519df6d5b9ea95483fc420a1ff1
--- /dev/null
+++ b/tests/value/oracle_equalities/audit.res.oracle
@@ -0,0 +1,11 @@
+1,8d0
+< [kernel:audit] Warning:
+< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101
+< [kernel:audit] Warning:
+< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list)
+< [kernel:audit] Warning:
+< missing files:
+< tests/value/non_existing_file.h
+< [kernel] Audit: sources list written to: tests/value/result/audit-out.json
+34d25
+< [kernel] Wrote: tests/value/result/audit-out.json
diff --git a/tests/value/oracle_equalities/auto_loop_unroll.0.res.oracle b/tests/value/oracle_equalities/auto_loop_unroll.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c4e3470add3e62e659d9d62f21c25c615c1a7e87
--- /dev/null
+++ b/tests/value/oracle_equalities/auto_loop_unroll.0.res.oracle
@@ -0,0 +1,14 @@
+81c81,84
+< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
+---
+> [eva] computing for function incr <- various_loops <- main.
+> Called from tests/value/auto_loop_unroll.c:101.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+90c93,96
+< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
+---
+> [eva] computing for function incr <- various_loops <- main.
+> Called from tests/value/auto_loop_unroll.c:101.
+> [eva] Recording results for incr
+> [eva] Done for function incr
diff --git a/tests/value/oracle_equalities/auto_loop_unroll.1.res.oracle b/tests/value/oracle_equalities/auto_loop_unroll.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/automalloc.res.oracle b/tests/value/oracle_equalities/automalloc.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/backward_add_ptr.res.oracle b/tests/value/oracle_equalities/backward_add_ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6d66348323e4bca303cc34ee043db630877b4540
--- /dev/null
+++ b/tests/value/oracle_equalities/backward_add_ptr.res.oracle
@@ -0,0 +1,116 @@
+12c12
+< Frama_C_show_each_only_a: {0; 1}, {{ &a }}, {0}
+---
+> Frama_C_show_each_only_a: {0}, {{ &a }}, {0}
+93c93,96
+< [eva] tests/value/backward_add_ptr.c:110: Reusing old results for call to gm
+---
+> [eva] computing for function gm <- main3 <- main.
+> Called from tests/value/backward_add_ptr.c:110.
+> [eva] Recording results for gm
+> [eva] Done for function gm
+107c110,113
+< [eva] tests/value/backward_add_ptr.c:125: Reusing old results for call to gm
+---
+> [eva] computing for function gm <- main3 <- main.
+> Called from tests/value/backward_add_ptr.c:125.
+> [eva] Recording results for gm
+> [eva] Done for function gm
+119c125
+< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
+---
+> (origin: Arithmetic Bottom) }},
+157,160c163,167
+< {{ garbled mix of &{b}
+< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
+< [0..4294967295]
+< [eva] tests/value/backward_add_ptr.c:160: Reusing old results for call to gm
+---
+> {{ garbled mix of &{b} (origin: Arithmetic Bottom) }}, [0..4294967295]
+> [eva] computing for function gm <- main4 <- main.
+> Called from tests/value/backward_add_ptr.c:160.
+> [eva] Recording results for gm
+> [eva] Done for function gm
+178c185
+< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
+---
+> (origin: Arithmetic Bottom) }},
+180c187
+< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }}
+---
+> (origin: Arithmetic Bottom) }}
+188c195
+< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }}
+---
+> (origin: Arithmetic Bottom) }}
+194c201
+< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
+---
+> (origin: Arithmetic Bottom) }},
+211a219,222
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:33}) }}
+> {{ garbled mix of &{a}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:33}) }}
+> {{ garbled mix of &{b}
+232a244,245
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:106}) }}
+234a248,251
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:107}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:115}) }}
+238c255,257
+< (origin: Arithmetic {tests/value/backward_add_ptr.c:115}) }}
+---
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:116}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:121}) }}
+240a260,263
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:122}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:130}) }}
+242a266,267
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:136}) }}
+245a271,272
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:137}) }}
+> {{ garbled mix of &{a; b}
+246a274,275
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:145}) }}
+248a278,285
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:150}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:151}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:156}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:157}) }}
+250a288,311
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:165}) }}
+> {{ garbled mix of &{b; c}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:165}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:166}) }}
+> {{ garbled mix of &{b; c}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:166}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:171}) }}
+> {{ garbled mix of &{b; c}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:171}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:172}) }}
+> {{ garbled mix of &{b; c}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:172}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:177}) }}
+> {{ garbled mix of &{b; c}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:177}) }}
+> {{ garbled mix of &{a; b}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:178}) }}
+> {{ garbled mix of &{b; c}
+> (origin: Arithmetic {tests/value/backward_add_ptr.c:178}) }}
diff --git a/tests/value/oracle_equalities/backward_arith.res.oracle b/tests/value/oracle_equalities/backward_arith.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bad_loop.res.oracle b/tests/value/oracle_equalities/bad_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/base_addr_offset_block_length.res.oracle b/tests/value/oracle_equalities/base_addr_offset_block_length.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/behavior_statuses.0.res.oracle b/tests/value/oracle_equalities/behavior_statuses.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/behavior_statuses.1.res.oracle b/tests/value/oracle_equalities/behavior_statuses.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/behaviors1.res.oracle b/tests/value/oracle_equalities/behaviors1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/behaviors2.res.oracle b/tests/value/oracle_equalities/behaviors2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/big_lib_entry.res.oracle b/tests/value/oracle_equalities/big_lib_entry.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bigarray.res.oracle b/tests/value/oracle_equalities/bigarray.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bitfield.res.oracle b/tests/value/oracle_equalities/bitfield.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..199dae9e57a2dd302735cfae290ce5e5f5788679
--- /dev/null
+++ b/tests/value/oracle_equalities/bitfield.res.oracle
@@ -0,0 +1,4 @@
+138a139,141
+> [eva] tests/value/bitfield.i:71:
+> Frama_C_show_each:
+> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
diff --git a/tests/value/oracle_equalities/bitfield_assign.res.oracle b/tests/value/oracle_equalities/bitfield_assign.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bitfield_longlong.res.oracle b/tests/value/oracle_equalities/bitfield_longlong.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bitfield_receives_result.res.oracle b/tests/value/oracle_equalities/bitfield_receives_result.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bitwise.res.oracle b/tests/value/oracle_equalities/bitwise.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bitwise_float.res.oracle b/tests/value/oracle_equalities/bitwise_float.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bitwise_pointer.res.oracle b/tests/value/oracle_equalities/bitwise_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f04f7077977a5a61ea7d346c6ff6f90a2e4237e4
--- /dev/null
+++ b/tests/value/oracle_equalities/bitwise_pointer.res.oracle
@@ -0,0 +1,8 @@
+62c62
+< x ∈ [0..9]
+---
+> x ∈ {5}
+75c75
+< x1 ∈ [0..9]
+---
+> x1 ∈ {5}
diff --git a/tests/value/oracle_equalities/bitwise_reduction.res.oracle b/tests/value/oracle_equalities/bitwise_reduction.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/biz.res.oracle b/tests/value/oracle_equalities/biz.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bool.res.oracle b/tests/value/oracle_equalities/bool.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/branch.res.oracle b/tests/value/oracle_equalities/branch.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/branch2.res.oracle b/tests/value/oracle_equalities/branch2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/broken_loop.res.oracle b/tests/value/oracle_equalities/broken_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bts0506.0.res.oracle b/tests/value/oracle_equalities/bts0506.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bts0506.1.res.oracle b/tests/value/oracle_equalities/bts0506.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bts0775.res.oracle b/tests/value/oracle_equalities/bts0775.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bts0858.res.oracle b/tests/value/oracle_equalities/bts0858.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bts1306.res.oracle b/tests/value/oracle_equalities/bts1306.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/buffer_overflow.0.res.oracle b/tests/value/oracle_equalities/buffer_overflow.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/buffer_overflow.1.res.oracle b/tests/value/oracle_equalities/buffer_overflow.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bug.res.oracle b/tests/value/oracle_equalities/bug.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bug0196.res.oracle b/tests/value/oracle_equalities/bug0196.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bug0223.0.res.oracle b/tests/value/oracle_equalities/bug0223.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bug0223.1.res.oracle b/tests/value/oracle_equalities/bug0223.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bug0245.res.oracle b/tests/value/oracle_equalities/bug0245.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bug_023.res.oracle b/tests/value/oracle_equalities/bug_023.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/bug_0244.res.oracle b/tests/value/oracle_equalities/bug_0244.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/builtins_split.res.oracle b/tests/value/oracle_equalities/builtins_split.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call.res.oracle b/tests/value/oracle_equalities/call.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_2.res.oracle b/tests/value/oracle_equalities/call_2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_3.res.oracle b/tests/value/oracle_equalities/call_3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_alias.0.res.oracle b/tests/value/oracle_equalities/call_alias.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_alias.1.res.oracle b/tests/value/oracle_equalities/call_alias.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_alias.2.res.oracle b/tests/value/oracle_equalities/call_alias.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_deep.res.oracle b/tests/value/oracle_equalities/call_deep.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_multi.res.oracle b/tests/value/oracle_equalities/call_multi.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/call_simple.res.oracle b/tests/value/oracle_equalities/call_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..74d12f1f99b9b00efad1a5bf4a6df343d225573b
--- /dev/null
+++ b/tests/value/oracle_equalities/call_simple.res.oracle
@@ -0,0 +1,4 @@
+28c28
+< c ∈ [--..--]
+---
+> c ∈ [-2147483648..2147483646]
diff --git a/tests/value/oracle_equalities/case_analysis.res.oracle b/tests/value/oracle_equalities/case_analysis.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..85985d3ff7dc7596f41c4a3b51f1614b76c5cfdb
--- /dev/null
+++ b/tests/value/oracle_equalities/case_analysis.res.oracle
@@ -0,0 +1,9 @@
+11a12,15
+> [eva] tests/value/case_analysis.i:18:
+> The evaluation of the expression r * r
+> led to bottom without alarms:
+> at this point the product of states has no possible concretization.
+18c22
+< rq ∈ [-0.0000000000000000 .. 100.0000000000000000]
+---
+> rq ∈ [0.0000000000000000 .. 100.0000000000000000]
diff --git a/tests/value/oracle_equalities/cast.res.oracle b/tests/value/oracle_equalities/cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cast1.res.oracle b/tests/value/oracle_equalities/cast1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cast2.res.oracle b/tests/value/oracle_equalities/cast2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cast_axalto.res.oracle b/tests/value/oracle_equalities/cast_axalto.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cast_fun.res.oracle b/tests/value/oracle_equalities/cast_fun.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cast_hetero.res.oracle b/tests/value/oracle_equalities/cast_hetero.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cast_return.0.res.oracle b/tests/value/oracle_equalities/cast_return.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cast_return.1.res.oracle b/tests/value/oracle_equalities/cast_return.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cert_exp35_c.res.oracle b/tests/value/oracle_equalities/cert_exp35_c.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/changeret.res.oracle b/tests/value/oracle_equalities/changeret.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cmp.res.oracle b/tests/value/oracle_equalities/cmp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cmp_ptr.0.res.oracle b/tests/value/oracle_equalities/cmp_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cmp_ptr.1.res.oracle b/tests/value/oracle_equalities/cmp_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cmp_ptr_follow_all_branches.0.res.oracle b/tests/value/oracle_equalities/cmp_ptr_follow_all_branches.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cmp_ptr_follow_all_branches.1.res.oracle b/tests/value/oracle_equalities/cmp_ptr_follow_all_branches.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cond.res.oracle b/tests/value/oracle_equalities/cond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cond2.0.res.oracle b/tests/value/oracle_equalities/cond2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cond2.1.res.oracle b/tests/value/oracle_equalities/cond2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/cond_integer_cast_of_float.res.oracle b/tests/value/oracle_equalities/cond_integer_cast_of_float.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/conditional_initializer.res.oracle b/tests/value/oracle_equalities/conditional_initializer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/const.res.oracle b/tests/value/oracle_equalities/const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/const2.res.oracle b/tests/value/oracle_equalities/const2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/const_syntax.res.oracle b/tests/value/oracle_equalities/const_syntax.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/const_typedef.res.oracle b/tests/value/oracle_equalities/const_typedef.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/constarraystructlibentry.res.oracle b/tests/value/oracle_equalities/constarraystructlibentry.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/context_free.res.oracle b/tests/value/oracle_equalities/context_free.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/context_free_simple.res.oracle b/tests/value/oracle_equalities/context_free_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/context_width.res.oracle b/tests/value/oracle_equalities/context_width.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/control.res.oracle b/tests/value/oracle_equalities/control.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/conversion.res.oracle b/tests/value/oracle_equalities/conversion.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/copy_paste.res.oracle b/tests/value/oracle_equalities/copy_paste.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/copy_paste_hidden_by_dummy_cast.res.oracle b/tests/value/oracle_equalities/copy_paste_hidden_by_dummy_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/copy_stdin.res.oracle b/tests/value/oracle_equalities/copy_stdin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/dangling.res.oracle b/tests/value/oracle_equalities/dangling.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/dataflow_order.res.oracle b/tests/value/oracle_equalities/dataflow_order.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/dead_code.res.oracle b/tests/value/oracle_equalities/dead_code.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/dead_code2.res.oracle b/tests/value/oracle_equalities/dead_code2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/dead_inout.res.oracle b/tests/value/oracle_equalities/dead_inout.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/dead_statuses.res.oracle b/tests/value/oracle_equalities/dead_statuses.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deep_conditionals.res.oracle b/tests/value/oracle_equalities/deep_conditionals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/degeneration2.res.oracle b/tests/value/oracle_equalities/degeneration2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps.0.res.oracle b/tests/value/oracle_equalities/deps.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps.1.res.oracle b/tests/value/oracle_equalities/deps.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps.2.res.oracle b/tests/value/oracle_equalities/deps.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps_addr.res.oracle b/tests/value/oracle_equalities/deps_addr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps_compose.res.oracle b/tests/value/oracle_equalities/deps_compose.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps_local.res.oracle b/tests/value/oracle_equalities/deps_local.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps_mixed.res.oracle b/tests/value/oracle_equalities/deps_mixed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deps_unitialized_locals.res.oracle b/tests/value/oracle_equalities/deps_unitialized_locals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/deref.res.oracle b/tests/value/oracle_equalities/deref.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/descending.res.oracle b/tests/value/oracle_equalities/descending.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4f7f74dacd94a03077b450e88028ef39d7764628
--- /dev/null
+++ b/tests/value/oracle_equalities/descending.res.oracle
@@ -0,0 +1,4 @@
+42c42
+< i ∈ {31; 32}
+---
+> i ∈ {31}
diff --git a/tests/value/oracle_equalities/disjoint_status.res.oracle b/tests/value/oracle_equalities/disjoint_status.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/div.0.res.oracle b/tests/value/oracle_equalities/div.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/div.1.res.oracle b/tests/value/oracle_equalities/div.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/div_strange.res.oracle b/tests/value/oracle_equalities/div_strange.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/divneg.res.oracle b/tests/value/oracle_equalities/divneg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/domains.res.oracle b/tests/value/oracle_equalities/domains.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/domains_function.res.oracle b/tests/value/oracle_equalities/domains_function.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a6b3f21d9de7b40fead8b5aea5d48b5e5c5fa4ba
--- /dev/null
+++ b/tests/value/oracle_equalities/domains_function.res.oracle
@@ -0,0 +1,61 @@
+19,20c19
+< [eva] tests/value/domains_function.c:92:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:92: Frama_C_show_each_top: {3}
+28,29c27
+< [eva] tests/value/domains_function.c:77:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
+32,33c30
+< [eva] tests/value/domains_function.c:96:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:96: Frama_C_show_each_top: {1}
+36,37c33
+< [eva] tests/value/domains_function.c:84:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:84: Frama_C_show_each_top: {2}
+40,41c36
+< [eva] tests/value/domains_function.c:98:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:98: Frama_C_show_each_top: {2}
+60,61c55
+< [eva] tests/value/domains_function.c:84:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:84: Frama_C_show_each_top: {2}
+64,65c58
+< [eva] tests/value/domains_function.c:113:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:113: Frama_C_show_each_top: {2}
+78,79c71
+< [eva] tests/value/domains_function.c:55:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:55: Frama_C_show_each_top: {42}
+108,109c100
+< [eva] tests/value/domains_function.c:64:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:64: Frama_C_show_each_top: {42}
+116c107
+< result ∈ [--..--]
+---
+> result ∈ {2}
+130c121
+< result ∈ [--..--]
+---
+> result ∈ {1}
+135c126
+< result ∈ [--..--]
+---
+> result ∈ {2}
+138c129
+< result ∈ [--..--]
+---
+> result ∈ {2}
diff --git a/tests/value/oracle_equalities/downcast.0.res.oracle b/tests/value/oracle_equalities/downcast.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/downcast.1.res.oracle b/tests/value/oracle_equalities/downcast.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/downcast.2.res.oracle b/tests/value/oracle_equalities/downcast.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3aac066cc202967755f0dd520cfe9db775c84554
--- /dev/null
+++ b/tests/value/oracle_equalities/downcast.2.res.oracle
@@ -0,0 +1,8 @@
+114c114
+< ux ∈ [--..--]
+---
+> ux ∈ [0..65535]
+157c157
+< ux ∈ [--..--]
+---
+> ux ∈ [0..65535]
diff --git a/tests/value/oracle_equalities/downcast.3.res.oracle b/tests/value/oracle_equalities/downcast.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/downcast.4.res.oracle b/tests/value/oracle_equalities/downcast.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/dur.res.oracle b/tests/value/oracle_equalities/dur.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_base.0.res.oracle b/tests/value/oracle_equalities/empty_base.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_base.1.res.oracle b/tests/value/oracle_equalities/empty_base.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct.0.res.oracle b/tests/value/oracle_equalities/empty_struct.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct.1.res.oracle b/tests/value/oracle_equalities/empty_struct.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct.2.res.oracle b/tests/value/oracle_equalities/empty_struct.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct.3.res.oracle b/tests/value/oracle_equalities/empty_struct.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct.4.res.oracle b/tests/value/oracle_equalities/empty_struct.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct.5.res.oracle b/tests/value/oracle_equalities/empty_struct.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct.6.res.oracle b/tests/value/oracle_equalities/empty_struct.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_struct2.res.oracle b/tests/value/oracle_equalities/empty_struct2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/empty_union.res.oracle b/tests/value/oracle_equalities/empty_union.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/endian.0.res.oracle b/tests/value/oracle_equalities/endian.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/endian.1.res.oracle b/tests/value/oracle_equalities/endian.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/enum.res.oracle b/tests/value/oracle_equalities/enum.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/enum2.res.oracle b/tests/value/oracle_equalities/enum2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/equality.res.oracle b/tests/value/oracle_equalities/equality.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/eval_separated.res.oracle b/tests/value/oracle_equalities/eval_separated.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/exit_paths.res.oracle b/tests/value/oracle_equalities/exit_paths.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/extern.res.oracle b/tests/value/oracle_equalities/extern.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/f1.res.oracle b/tests/value/oracle_equalities/f1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/f2.res.oracle b/tests/value/oracle_equalities/f2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/false.res.oracle b/tests/value/oracle_equalities/false.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/fam_sizeof.res.oracle b/tests/value/oracle_equalities/fam_sizeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/find_ivaltop.res.oracle b/tests/value/oracle_equalities/find_ivaltop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/folding.res.oracle b/tests/value/oracle_equalities/folding.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/for_loops.0.res.oracle b/tests/value/oracle_equalities/for_loops.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/for_loops.1.res.oracle b/tests/value/oracle_equalities/for_loops.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/for_loops.2.res.oracle b/tests/value/oracle_equalities/for_loops.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/for_loops.3.res.oracle b/tests/value/oracle_equalities/for_loops.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/forall.res.oracle b/tests/value/oracle_equalities/forall.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/fptr.0.res.oracle b/tests/value/oracle_equalities/fptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/fptr.1.res.oracle b/tests/value/oracle_equalities/fptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ce2032c08e6534394dd65b70b6f5af021684d613
--- /dev/null
+++ b/tests/value/oracle_equalities/fptr.1.res.oracle
@@ -0,0 +1,8 @@
+55,57d54
+< [eva] tests/value/fptr.i:67:
+< Frama_C_show_each_F: {{ NULL + [0..4294967295] ; &h ; &hh }}
+< [eva] tests/value/fptr.i:68: Reusing old results for call to f
+69c66
+< n ∈ {0; 1; 2}
+---
+> n ∈ {0; 1}
diff --git a/tests/value/oracle_equalities/from1.res.oracle b/tests/value/oracle_equalities/from1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_call.0.res.oracle b/tests/value/oracle_equalities/from_call.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..112d7de0bf83f985282dc85dcc11b8f3fa2f6ae5
--- /dev/null
+++ b/tests/value/oracle_equalities/from_call.0.res.oracle
@@ -0,0 +1,18 @@
+68c68,73
+< [eva] tests/value/from_call.i:20: Reusing old results for call to g
+---
+> [eva] computing for function g <- f <- main.
+> Called from tests/value/from_call.i:20.
+> [eva] Recording results for g
+> [from] Computing for function g
+> [from] Done for function g
+> [eva] Done for function g
+78c83,88
+< [eva] tests/value/from_call.i:20: Reusing old results for call to g
+---
+> [eva] computing for function g <- f <- main.
+> Called from tests/value/from_call.i:20.
+> [eva] Recording results for g
+> [from] Computing for function g
+> [from] Done for function g
+> [eva] Done for function g
diff --git a/tests/value/oracle_equalities/from_call.1.res.oracle b/tests/value/oracle_equalities/from_call.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9affe79cca9f4bf6f13817bdc5a9b1ae11fc72ea
--- /dev/null
+++ b/tests/value/oracle_equalities/from_call.1.res.oracle
@@ -0,0 +1,14 @@
+64c64,67
+< [eva] tests/value/from_call.i:20: Reusing old results for call to g
+---
+> [eva] computing for function g <- f <- main.
+> Called from tests/value/from_call.i:20.
+> [eva] Recording results for g
+> [eva] Done for function g
+72c75,78
+< [eva] tests/value/from_call.i:20: Reusing old results for call to g
+---
+> [eva] computing for function g <- f <- main.
+> Called from tests/value/from_call.i:20.
+> [eva] Recording results for g
+> [eva] Done for function g
diff --git a/tests/value/oracle_equalities/from_global.res.oracle b/tests/value/oracle_equalities/from_global.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_ind.res.oracle b/tests/value/oracle_equalities/from_ind.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.0.res.oracle b/tests/value/oracle_equalities/from_pb.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.1.res.oracle b/tests/value/oracle_equalities/from_pb.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.2.res.oracle b/tests/value/oracle_equalities/from_pb.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.3.res.oracle b/tests/value/oracle_equalities/from_pb.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.4.res.oracle b/tests/value/oracle_equalities/from_pb.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.5.res.oracle b/tests/value/oracle_equalities/from_pb.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.6.res.oracle b/tests/value/oracle_equalities/from_pb.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_pb.7.res.oracle b/tests/value/oracle_equalities/from_pb.7.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_ptr.0.res.oracle b/tests/value/oracle_equalities/from_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_ptr.1.res.oracle b/tests/value/oracle_equalities/from_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_ptr2.res.oracle b/tests/value/oracle_equalities/from_ptr2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_res_2.res.oracle b/tests/value/oracle_equalities/from_res_2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/from_termin.res.oracle b/tests/value/oracle_equalities/from_termin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a29f1796862a617621451045df13187bf62b6a6d
--- /dev/null
+++ b/tests/value/oracle_equalities/from_termin.res.oracle
@@ -0,0 +1,2 @@
+9a10
+> [eva] tests/value/from_termin.i:8: starting to merge loop iterations
diff --git a/tests/value/oracle_equalities/fun_ptr.0.res.oracle b/tests/value/oracle_equalities/fun_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/fun_ptr.1.res.oracle b/tests/value/oracle_equalities/fun_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/function_return_serial_casts.res.oracle b/tests/value/oracle_equalities/function_return_serial_casts.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/g1.res.oracle b/tests/value/oracle_equalities/g1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/garbled_init.res.oracle b/tests/value/oracle_equalities/garbled_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/gauges.res.oracle b/tests/value/oracle_equalities/gauges.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ghost.res.oracle b/tests/value/oracle_equalities/ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/global_bug.res.oracle b/tests/value/oracle_equalities/global_bug.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/goto.res.oracle b/tests/value/oracle_equalities/goto.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/hierarchical_convergence.res.oracle b/tests/value/oracle_equalities/hierarchical_convergence.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/if.0.res.oracle b/tests/value/oracle_equalities/if.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/if.1.res.oracle b/tests/value/oracle_equalities/if.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/if2.res.oracle b/tests/value/oracle_equalities/if2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ilevel.res.oracle b/tests/value/oracle_equalities/ilevel.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/implies.res.oracle b/tests/value/oracle_equalities/implies.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/imprecise_invalid_write.res.oracle b/tests/value/oracle_equalities/imprecise_invalid_write.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..911514fc0b77252b400c11e7c5c9d44daef55de9
--- /dev/null
+++ b/tests/value/oracle_equalities/imprecise_invalid_write.res.oracle
@@ -0,0 +1,3 @@
+29a30,31
+> [kernel] tests/value/imprecise_invalid_write.i:9:
+> imprecise size for variable main1 (Undefined sizeof on a function.)
diff --git a/tests/value/oracle_equalities/incompatible_states.res.oracle b/tests/value/oracle_equalities/incompatible_states.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7126073f2df44b792e5e3436846684d856469863
--- /dev/null
+++ b/tests/value/oracle_equalities/incompatible_states.res.oracle
@@ -0,0 +1,29 @@
+14a15,18
+> [eva] tests/value/incompatible_states.c:24:
+> The evaluation of the expression x * x
+> led to bottom without alarms:
+> at this point the product of states has no possible concretization.
+27,29c31,34
+< [eva:alarm] tests/value/incompatible_states.c:41: Warning:
+< accessing uninitialized left-value.
+< assert \initialized(&t[(int)((int)(2 * i) / 2)]);
+---
+> [eva] tests/value/incompatible_states.c:41:
+> The evaluation of the expression t[(2 * i) / 2]
+> led to bottom without alarms:
+> at this point the product of states has no possible concretization.
+41,42d45
+< [eva:alarm] tests/value/incompatible_states.c:53: Warning:
+< division by zero. assert t[i] ≢ 0;
+47,49d49
+< [eva] tests/value/incompatible_states.c:41:
+< assertion 'Eva,initialization' got final status invalid.
+< [scope:rm_asserts] removing 2 assertion(s)
+55c55
+< z ∈ [-3..100]
+---
+> z ∈ {-3; -2}
+58c58
+< t[0] ∈ {0; 1}
+---
+> t[0] ∈ {0}
diff --git a/tests/value/oracle_equalities/incorrect_reduce_expr.res.oracle b/tests/value/oracle_equalities/incorrect_reduce_expr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ineq.res.oracle b/tests/value/oracle_equalities/ineq.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/infinite.res.oracle b/tests/value/oracle_equalities/infinite.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/init.0.res.oracle b/tests/value/oracle_equalities/init.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/init.1.res.oracle b/tests/value/oracle_equalities/init.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/init_const_guard.res.oracle b/tests/value/oracle_equalities/init_const_guard.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/initialized.res.oracle b/tests/value/oracle_equalities/initialized.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/initialized_copy.0.res.oracle b/tests/value/oracle_equalities/initialized_copy.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/initialized_copy.1.res.oracle b/tests/value/oracle_equalities/initialized_copy.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout.0.res.oracle b/tests/value/oracle_equalities/inout.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout.1.res.oracle b/tests/value/oracle_equalities/inout.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout.2.res.oracle b/tests/value/oracle_equalities/inout.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout.3.res.oracle b/tests/value/oracle_equalities/inout.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout.4.res.oracle b/tests/value/oracle_equalities/inout.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout_diff.res.oracle b/tests/value/oracle_equalities/inout_diff.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout_formals.res.oracle b/tests/value/oracle_equalities/inout_formals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout_on_alarms.res.oracle b/tests/value/oracle_equalities/inout_on_alarms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inout_proto.res.oracle b/tests/value/oracle_equalities/inout_proto.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/input.res.oracle b/tests/value/oracle_equalities/input.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/integers.res.oracle b/tests/value/oracle_equalities/integers.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/interpol.res.oracle b/tests/value/oracle_equalities/interpol.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/interpreter-mode-syracuse.res.oracle b/tests/value/oracle_equalities/interpreter-mode-syracuse.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/invalid_loc_return.res.oracle b/tests/value/oracle_equalities/invalid_loc_return.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/invalid_lval_arg.res.oracle b/tests/value/oracle_equalities/invalid_lval_arg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/invalid_pointer.0.res.oracle b/tests/value/oracle_equalities/invalid_pointer.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/invalid_pointer.1.res.oracle b/tests/value/oracle_equalities/invalid_pointer.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inversion.res.oracle b/tests/value/oracle_equalities/inversion.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/inversion2.res.oracle b/tests/value/oracle_equalities/inversion2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/jacques.res.oracle b/tests/value/oracle_equalities/jacques.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/join_misaligned.res.oracle b/tests/value/oracle_equalities/join_misaligned.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/label.res.oracle b/tests/value/oracle_equalities/label.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/lazy.0.res.oracle b/tests/value/oracle_equalities/lazy.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/lazy.1.res.oracle b/tests/value/oracle_equalities/lazy.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/leaf.res.oracle b/tests/value/oracle_equalities/leaf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/leaf2.res.oracle b/tests/value/oracle_equalities/leaf2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/leaf_spec.0.res.oracle b/tests/value/oracle_equalities/leaf_spec.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/leaf_spec.1.res.oracle b/tests/value/oracle_equalities/leaf_spec.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/library.res.oracle b/tests/value/oracle_equalities/library.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..263da140a44605a2369da667c8975a15feee5d56
--- /dev/null
+++ b/tests/value/oracle_equalities/library.res.oracle
@@ -0,0 +1,5 @@
+129,132d128
+< [eva:alarm] tests/value/library.i:44: Warning:
+< non-finite float value. assert \is_finite(*pf);
+< [eva:alarm] tests/value/library.i:44: Warning:
+< non-finite float value. assert \is_finite(\add_float(*pf, *pf));
diff --git a/tests/value/oracle_equalities/library_precond.res.oracle b/tests/value/oracle_equalities/library_precond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/limits.res.oracle b/tests/value/oracle_equalities/limits.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/local.res.oracle b/tests/value/oracle_equalities/local.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/local_cleanup.res.oracle b/tests/value/oracle_equalities/local_cleanup.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/local_slevel.res.oracle b/tests/value/oracle_equalities/local_slevel.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/local_variables.res.oracle b/tests/value/oracle_equalities/local_variables.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/lock.res.oracle b/tests/value/oracle_equalities/lock.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/logic.res.oracle b/tests/value/oracle_equalities/logic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/logic_ptr_cast.res.oracle b/tests/value/oracle_equalities/logic_ptr_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/logicdeps.res.oracle b/tests/value/oracle_equalities/logicdeps.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/long.res.oracle b/tests/value/oracle_equalities/long.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/long_const.0.res.oracle b/tests/value/oracle_equalities/long_const.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9bc5f2d7083802aa0ac216e8eaeca4c1be79eeb8
--- /dev/null
+++ b/tests/value/oracle_equalities/long_const.0.res.oracle
@@ -0,0 +1,7 @@
+19c19,22
+< [eva] tests/value/long_const.i:25: Reusing old results for call to LL_ABS
+---
+> [eva] computing for function LL_ABS <- div64 <- main.
+> Called from tests/value/long_const.i:25.
+> [eva] Recording results for LL_ABS
+> [eva] Done for function LL_ABS
diff --git a/tests/value/oracle_equalities/long_const.1.res.oracle b/tests/value/oracle_equalities/long_const.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9bc5f2d7083802aa0ac216e8eaeca4c1be79eeb8
--- /dev/null
+++ b/tests/value/oracle_equalities/long_const.1.res.oracle
@@ -0,0 +1,7 @@
+19c19,22
+< [eva] tests/value/long_const.i:25: Reusing old results for call to LL_ABS
+---
+> [eva] computing for function LL_ABS <- div64 <- main.
+> Called from tests/value/long_const.i:25.
+> [eva] Recording results for LL_ABS
+> [eva] Done for function LL_ABS
diff --git a/tests/value/oracle_equalities/loop.res.oracle b/tests/value/oracle_equalities/loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop1.res.oracle b/tests/value/oracle_equalities/loop1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop2.res.oracle b/tests/value/oracle_equalities/loop2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop3.res.oracle b/tests/value/oracle_equalities/loop3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_array.res.oracle b/tests/value/oracle_equalities/loop_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_join.res.oracle b/tests/value/oracle_equalities/loop_join.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_long.res.oracle b/tests/value/oracle_equalities/loop_long.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_no_var.res.oracle b/tests/value/oracle_equalities/loop_no_var.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_simple.res.oracle b/tests/value/oracle_equalities/loop_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_test.0.res.oracle b/tests/value/oracle_equalities/loop_test.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_test.1.res.oracle b/tests/value/oracle_equalities/loop_test.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_wvar.0.res.oracle b/tests/value/oracle_equalities/loop_wvar.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_wvar.1.res.oracle b/tests/value/oracle_equalities/loop_wvar.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_wvar.2.res.oracle b/tests/value/oracle_equalities/loop_wvar.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loop_wvar.3.res.oracle b/tests/value/oracle_equalities/loop_wvar.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loopfun.0.res.oracle b/tests/value/oracle_equalities/loopfun.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loopfun.1.res.oracle b/tests/value/oracle_equalities/loopfun.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/loopinv.res.oracle b/tests/value/oracle_equalities/loopinv.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/machdep.res.oracle b/tests/value/oracle_equalities/machdep.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/max_pointed.res.oracle b/tests/value/oracle_equalities/max_pointed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/memexec.res.oracle b/tests/value/oracle_equalities/memexec.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/merge_bits.res.oracle b/tests/value/oracle_equalities/merge_bits.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/mini_pointrer.res.oracle b/tests/value/oracle_equalities/mini_pointrer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/misaligned_tabs.res.oracle b/tests/value/oracle_equalities/misaligned_tabs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/mixed_val.res.oracle b/tests/value/oracle_equalities/mixed_val.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/modifies.res.oracle b/tests/value/oracle_equalities/modifies.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/modulo.res.oracle b/tests/value/oracle_equalities/modulo.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..750dc4d69d0be5d70fb5ddd65b953ecba6b8837a
--- /dev/null
+++ b/tests/value/oracle_equalities/modulo.res.oracle
@@ -0,0 +1,174 @@
+40a41,119
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-8; -7; -6; -5; -4; -3; -2; -1},
+> {-7; -6; -5; -4; -3; -2; -1},
+> {-6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-8; -7; -6; -5; -4; -3; -2; -1},
+> {1; 2; 3; 4; 5; 6; 7},
+> {-6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-7; -6; -5; -4; -3; -2; -1},
+> {-6; -5; -4; -3; -2; -1},
+> {-5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {1; 2}, {0; 1}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {-3; -2; -1}, {1; 2}, {-1; 0}
+> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {-2; -1}, {0; 1}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {-3; -2; -1}, {-2; -1}, {-1; 0}
+50a130,208
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {-8; -7; -6; -5; -4; -3; -2; -1},
+> {1; 2; 3; 4; 5; 6; 7},
+> {-6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {-8; -7; -6; -5; -4; -3; -2; -1},
+> {-7; -6; -5; -4; -3; -2; -1},
+> {-6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {-7; -6; -5; -4; -3; -2; -1},
+> {-6; -5; -4; -3; -2; -1},
+> {-5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2:
+> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {-3; -2; -1}, {1; 2}, {-1; 0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
+> [eva] tests/value/modulo.i:53:
+> Frama_C_show_each_2: {-3; -2; -1}, {-2; -1}, {-1; 0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
+60a219,231
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-8..8], [-7..7], [-6..6]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-7..7], [-6..6], [-5..5]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-6..6], [-5..5], [-4..4]
+> [eva] tests/value/modulo.i:64:
+> Frama_C_show_each_3:
+> [-5..5], {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 0; 1; 2; 3}
+> [eva] tests/value/modulo.i:64:
+> Frama_C_show_each_3:
+> {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 1; 2; 3}, {-2; -1; 0; 1; 2}
+> [eva] tests/value/modulo.i:64:
+> Frama_C_show_each_3: {-3; -2; -1; 1; 2; 3}, {-2; -1; 1; 2}, {-1; 0; 1}
diff --git a/tests/value/oracle_equalities/multi_access.res.oracle b/tests/value/oracle_equalities/multi_access.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/narrow_behaviors.res.oracle b/tests/value/oracle_equalities/narrow_behaviors.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/nested_struct_init.res.oracle b/tests/value/oracle_equalities/nested_struct_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/no_results.res.oracle b/tests/value/oracle_equalities/no_results.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/non_iso_initializer.res.oracle b/tests/value/oracle_equalities/non_iso_initializer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/non_natural.res.oracle b/tests/value/oracle_equalities/non_natural.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e2a7857fd096431f5c785683670a882ab38da5c1
--- /dev/null
+++ b/tests/value/oracle_equalities/non_natural.res.oracle
@@ -0,0 +1,52 @@
+58a59,60
+> [kernel] tests/value/non_natural.i:30:
+> more than 200(12500) elements to enumerate. Approximating.
+65a68,71
+> [kernel] tests/value/non_natural.i:23:
+> more than 200(12500) elements to enumerate. Approximating.
+> [kernel] tests/value/non_natural.i:23:
+> more than 200(12501) elements to enumerate. Approximating.
+70a77,80
+> [kernel] tests/value/non_natural.i:24:
+> more than 200(12500) elements to enumerate. Approximating.
+> [kernel] tests/value/non_natural.i:24:
+> more than 200(12501) elements to enumerate. Approximating.
+78a89,90
+> [kernel] tests/value/non_natural.i:25:
+> more than 200(12500) elements to enumerate. Approximating.
+86a99,100
+> [kernel] tests/value/non_natural.i:26:
+> more than 200(12500) elements to enumerate. Approximating.
+94a109,110
+> [kernel] tests/value/non_natural.i:27:
+> more than 200(12500) elements to enumerate. Approximating.
+102a119,120
+> [kernel] tests/value/non_natural.i:28:
+> more than 200(12500) elements to enumerate. Approximating.
+110a129,130
+> [kernel] tests/value/non_natural.i:29:
+> more than 200(12500) elements to enumerate. Approximating.
+127,146d146
+< [kernel] tests/value/non_natural.i:23:
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:23:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:24:
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:24:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:25:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:26:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:27:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:28:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:29:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:30:
+< more than 200(12500) elements to enumerate. Approximating.
+199a200,201
+> [kernel] tests/value/non_natural.i:39:
+> more than 200(12500) elements to enumerate. Approximating.
diff --git a/tests/value/oracle_equalities/nonlin.res.oracle b/tests/value/oracle_equalities/nonlin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6dd8e0102fc2e3d478beda8f9230a92167ddc615
--- /dev/null
+++ b/tests/value/oracle_equalities/nonlin.res.oracle
@@ -0,0 +1,4 @@
+194c194
+< q ∈ {{ &x + [-400..400],0%4 }}
+---
+> q ∈ {{ &x }}
diff --git a/tests/value/oracle_equalities/noreturn.res.oracle b/tests/value/oracle_equalities/noreturn.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/not.res.oracle b/tests/value/oracle_equalities/not.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/not_ct_array_arg.res.oracle b/tests/value/oracle_equalities/not_ct_array_arg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/null_lt_valid.res.oracle b/tests/value/oracle_equalities/null_lt_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/octagons.res.oracle b/tests/value/oracle_equalities/octagons.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8e32fb27d1dae1fdc6f8a36f2913f5e370871108
--- /dev/null
+++ b/tests/value/oracle_equalities/octagons.res.oracle
@@ -0,0 +1,8 @@
+29c29
+< Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+---
+> Frama_C_show_each_unreduced_unsigned: [0..4294967295], [6..4294967295]
+269c269
+< t ∈ [--..--] or UNINITIALIZED
+---
+> t ∈ [6..4294967295] or UNINITIALIZED
diff --git a/tests/value/oracle_equalities/offset_misaligned.res.oracle b/tests/value/oracle_equalities/offset_misaligned.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/offset_neg.res.oracle b/tests/value/oracle_equalities/offset_neg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/offset_top.res.oracle b/tests/value/oracle_equalities/offset_top.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/offsetmap.0.res.oracle b/tests/value/oracle_equalities/offsetmap.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6bebb89e738e4c6703b3d8b869f9d852e34a9e44
--- /dev/null
+++ b/tests/value/oracle_equalities/offsetmap.0.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
diff --git a/tests/value/oracle_equalities/offsetmap.1.res.oracle b/tests/value/oracle_equalities/offsetmap.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6bebb89e738e4c6703b3d8b869f9d852e34a9e44
--- /dev/null
+++ b/tests/value/oracle_equalities/offsetmap.1.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
diff --git a/tests/value/oracle_equalities/origin.0.res.oracle b/tests/value/oracle_equalities/origin.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..29915b28f57735ddab40f6179e5b5b12fe8a68b6
--- /dev/null
+++ b/tests/value/oracle_equalities/origin.0.res.oracle
@@ -0,0 +1,10 @@
+249,250c249
+< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
+< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
+---
+> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
+289,290c288
+< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
+< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
+---
+> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
diff --git a/tests/value/oracle_equalities/origin.1.res.oracle b/tests/value/oracle_equalities/origin.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/output_leafs.res.oracle b/tests/value/oracle_equalities/output_leafs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/overflow.0.res.oracle b/tests/value/oracle_equalities/overflow.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/overflow.1.res.oracle b/tests/value/oracle_equalities/overflow.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/overflow_cast_float_int.res.oracle b/tests/value/oracle_equalities/overflow_cast_float_int.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/packed.res.oracle b/tests/value/oracle_equalities/packed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/partitioning-annots.0.res.oracle b/tests/value/oracle_equalities/partitioning-annots.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/partitioning-annots.1.res.oracle b/tests/value/oracle_equalities/partitioning-annots.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/partitioning-annots.2.res.oracle b/tests/value/oracle_equalities/partitioning-annots.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/partitioning-annots.3.res.oracle b/tests/value/oracle_equalities/partitioning-annots.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/partitioning-annots.4.res.oracle b/tests/value/oracle_equalities/partitioning-annots.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/partitioning-annots.5.res.oracle b/tests/value/oracle_equalities/partitioning-annots.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/partitioning-annots.6.res.oracle b/tests/value/oracle_equalities/partitioning-annots.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pb.res.oracle b/tests/value/oracle_equalities/pb.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/period.res.oracle b/tests/value/oracle_equalities/period.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..99204176fa41dc5a9ee1e72337d2436541654499
--- /dev/null
+++ b/tests/value/oracle_equalities/period.res.oracle
@@ -0,0 +1,10 @@
+88,94d87
+< [eva:alarm] tests/value/period.c:53: Warning:
+< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
+< [eva] tests/value/period.c:53:
+< Assigning imprecise value to p.
+< The imprecision originates from Arithmetic {tests/value/period.c:53}
+< [eva:alarm] tests/value/period.c:54: Warning:
+< out of bounds read. assert \valid_read(p);
+99d91
+< [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle_equalities/plevel.res.oracle b/tests/value/oracle_equalities/plevel.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d19a038f2cb62353c97e3e6ede7f83a949ef654e
--- /dev/null
+++ b/tests/value/oracle_equalities/plevel.res.oracle
@@ -0,0 +1,4 @@
+12d11
+< [eva] Recording results for main
+14a14
+> [eva] Recording results for main
diff --git a/tests/value/oracle_equalities/pointer.res.oracle b/tests/value/oracle_equalities/pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer2.0.res.oracle b/tests/value/oracle_equalities/pointer2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer2.1.res.oracle b/tests/value/oracle_equalities/pointer2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer3.res.oracle b/tests/value/oracle_equalities/pointer3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer4.res.oracle b/tests/value/oracle_equalities/pointer4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer_arg.res.oracle b/tests/value/oracle_equalities/pointer_arg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer_comp.res.oracle b/tests/value/oracle_equalities/pointer_comp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d0e8bccda7d9e05b4aaebb9ccadc7b173769c729
--- /dev/null
+++ b/tests/value/oracle_equalities/pointer_comp.res.oracle
@@ -0,0 +1,5 @@
+30a31,34
+> [kernel] tests/value/pointer_comp.c:43:
+> imprecise size for variable g (Undefined sizeof on a function.)
+> [kernel] tests/value/pointer_comp.c:43:
+> imprecise size for variable f (Undefined sizeof on a function.)
diff --git a/tests/value/oracle_equalities/pointer_comparison.0.res.oracle b/tests/value/oracle_equalities/pointer_comparison.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer_comparison.1.res.oracle b/tests/value/oracle_equalities/pointer_comparison.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer_int_cast.res.oracle b/tests/value/oracle_equalities/pointer_int_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pointer_loop.res.oracle b/tests/value/oracle_equalities/pointer_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/postcond_leaf.res.oracle b/tests/value/oracle_equalities/postcond_leaf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/postcondition.res.oracle b/tests/value/oracle_equalities/postcondition.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pragma.res.oracle b/tests/value/oracle_equalities/pragma.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/precise_locations.res.oracle b/tests/value/oracle_equalities/precise_locations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/precond.res.oracle b/tests/value/oracle_equalities/precond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/precond2.0.res.oracle b/tests/value/oracle_equalities/precond2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/precond2.1.res.oracle b/tests/value/oracle_equalities/precond2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/propagate_bottom.res.oracle b/tests/value/oracle_equalities/propagate_bottom.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/protomain.res.oracle b/tests/value/oracle_equalities/protomain.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ptr_call_object.res.oracle b/tests/value/oracle_equalities/ptr_call_object.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ptr_relation.0.res.oracle b/tests/value/oracle_equalities/ptr_relation.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0ae744ec7d6e6fcde013d15696dcf66e9f1424b5
--- /dev/null
+++ b/tests/value/oracle_equalities/ptr_relation.0.res.oracle
@@ -0,0 +1,4 @@
+23c23
+< i ∈ {0; 77; 333}
+---
+> i ∈ {77}
diff --git a/tests/value/oracle_equalities/ptr_relation.1.res.oracle b/tests/value/oracle_equalities/ptr_relation.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ptr_relation.2.res.oracle b/tests/value/oracle_equalities/ptr_relation.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/pure_exp.res.oracle b/tests/value/oracle_equalities/pure_exp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/qualified_arrays.res.oracle b/tests/value/oracle_equalities/qualified_arrays.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/raz.res.oracle b/tests/value/oracle_equalities/raz.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/reading_null.res.oracle b/tests/value/oracle_equalities/reading_null.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/rec.res.oracle b/tests/value/oracle_equalities/rec.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/recol.0.res.oracle b/tests/value/oracle_equalities/recol.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/recol.1.res.oracle b/tests/value/oracle_equalities/recol.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/recursion.0.res.oracle b/tests/value/oracle_equalities/recursion.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/recursion.1.res.oracle b/tests/value/oracle_equalities/recursion.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/recursion2.res.oracle b/tests/value/oracle_equalities/recursion2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/reduce_by_valid.res.oracle b/tests/value/oracle_equalities/reduce_by_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/reduce_formals.res.oracle b/tests/value/oracle_equalities/reduce_formals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/reduce_index.res.oracle b/tests/value/oracle_equalities/reduce_index.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/reduce_valid.res.oracle b/tests/value/oracle_equalities/reduce_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/redundant_alarms.res.oracle b/tests/value/oracle_equalities/redundant_alarms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f5e5f009673c3c5e27ad9ea5cad16f50d7658123
--- /dev/null
+++ b/tests/value/oracle_equalities/redundant_alarms.res.oracle
@@ -0,0 +1,26 @@
+10,13d9
+< [eva:alarm] tests/value/redundant_alarms.c:11: Warning:
+< accessing uninitialized left-value. assert \initialized(p);
+< [eva:alarm] tests/value/redundant_alarms.c:12: Warning:
+< accessing uninitialized left-value. assert \initialized(p);
+24,25d19
+< [eva:alarm] tests/value/redundant_alarms.c:21: Warning:
+< accessing uninitialized left-value. assert \initialized(&t[i]);
+63,65c57
+< [scope:rm_asserts] removing 3 assertion(s)
+< [scope:rm_asserts] tests/value/redundant_alarms.c:12:
+< removing redundant assert Eva: initialization: \initialized(p);
+---
+> [scope:rm_asserts] removing 2 assertion(s)
+108d99
+< /*@ assert Eva: initialization: \initialized(p); */
+110d100
+< /*@ assert Eva: initialization: \initialized(p); */
+127d116
+< /*@ assert Eva: initialization: \initialized(&t[i]); */
+196a186
+> int z;
+199,201d188
+< *p = 1;
+< int z = *p + 1;
+< int w = *p + 2;
diff --git a/tests/value/oracle_equalities/reevaluate_alarms.res.oracle b/tests/value/oracle_equalities/reevaluate_alarms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/relation_reduction.res.oracle b/tests/value/oracle_equalities/relation_reduction.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..652ddf13af23bbb7e14fe2d38db7906e17bb7743
--- /dev/null
+++ b/tests/value/oracle_equalities/relation_reduction.res.oracle
@@ -0,0 +1,23 @@
+24,27d23
+< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
+< accessing out of bounds index. assert 0 ≤ y;
+< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
+< accessing out of bounds index. assert y < 9;
+34,37c30,33
+< R1 ∈ [-2147483648..2147483637]
+< R2 ∈ [-2147483638..2147483647]
+< R3 ∈ [--..--]
+< R4 ∈ {0; 1; 2; 3; 4; 5}
+---
+> R1 ∈ {0; 2}
+> R2 ∈ {0; 12}
+> R3 ∈ {0; 7}
+> R4 ∈ {0; 2}
+48c44
+< R4 FROM tab[0..8]; x (and SELF)
+---
+> R4 FROM tab[0..5]; x (and SELF)
+53c49
+< y; t; tab[0..8]
+---
+> y; t; tab[0..5]
diff --git a/tests/value/oracle_equalities/relation_shift.res.oracle b/tests/value/oracle_equalities/relation_shift.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7176e3f6955ca3876a5937202f9c1229c5a22c32
--- /dev/null
+++ b/tests/value/oracle_equalities/relation_shift.res.oracle
@@ -0,0 +1,12 @@
+35,36c35,36
+< x ∈ [-2147483647..2147483647]
+< y ∈ [-2147483648..2147483646]
+---
+> x ∈ [-2147483647..2147483642]
+> y ∈ [-2147483648..2147483645]
+53,54c53,54
+< x ∈ [-2147483647..2147483647]
+< y ∈ [-2147483648..2147483646]
+---
+> x ∈ [-2147483647..2147483642]
+> y ∈ [-2147483648..2147483645]
diff --git a/tests/value/oracle_equalities/relations.res.oracle b/tests/value/oracle_equalities/relations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4617cf21e379162224ce9806eb48d3cb6c53028c
--- /dev/null
+++ b/tests/value/oracle_equalities/relations.res.oracle
@@ -0,0 +1,15 @@
+60,61c60
+< u[0] ∈ [-2147483648..2147483646]
+< [1] ∈ [--..--]
+---
+> u[0..1] ∈ [-2147483648..2147483646]
+67,70c66,69
+< R1 ∈ [--..--]
+< R2 ∈ [--..--]
+< R3 ∈ [-2147483648..2147483646]
+< R4 ∈ [--..--]
+---
+> R1 ∈ {0; 3}
+> R2 ∈ {0; 3}
+> R3 ∈ {0; 2}
+> R4 ∈ {0; 2}
diff --git a/tests/value/oracle_equalities/relations2.res.oracle b/tests/value/oracle_equalities/relations2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..32e93421cc32a6ba5dcb1abdc57227c321db7b1c
--- /dev/null
+++ b/tests/value/oracle_equalities/relations2.res.oracle
@@ -0,0 +1,6 @@
+59c59
+< n ∈ [0..512]
+---
+> n ∈ [1..512]
+133d132
+< [eva] tests/value/relations2.i:57: Frama_C_show_each_NO2:
diff --git a/tests/value/oracle_equalities/relations_difficult.res.oracle b/tests/value/oracle_equalities/relations_difficult.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/replace_by_show_each.res.oracle b/tests/value/oracle_equalities/replace_by_show_each.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/resolve.res.oracle b/tests/value/oracle_equalities/resolve.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/return.res.oracle b/tests/value/oracle_equalities/return.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/semaphore.res.oracle b/tests/value/oracle_equalities/semaphore.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/separated.res.oracle b/tests/value/oracle_equalities/separated.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/shift.0.res.oracle b/tests/value/oracle_equalities/shift.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/shift.1.res.oracle b/tests/value/oracle_equalities/shift.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/shift_big.res.oracle b/tests/value/oracle_equalities/shift_big.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/shift_neg.0.res.oracle b/tests/value/oracle_equalities/shift_neg.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/shift_neg.1.res.oracle b/tests/value/oracle_equalities/shift_neg.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/sign_of_bitfiled_int.0.res.oracle b/tests/value/oracle_equalities/sign_of_bitfiled_int.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/sign_of_bitfiled_int.1.res.oracle b/tests/value/oracle_equalities/sign_of_bitfiled_int.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/simple_packed.res.oracle b/tests/value/oracle_equalities/simple_packed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/simple_path.res.oracle b/tests/value/oracle_equalities/simple_path.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/simplify_cfg.0.res.oracle b/tests/value/oracle_equalities/simplify_cfg.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/simplify_cfg.1.res.oracle b/tests/value/oracle_equalities/simplify_cfg.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/sizeof.res.oracle b/tests/value/oracle_equalities/sizeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/slevel_return.res.oracle b/tests/value/oracle_equalities/slevel_return.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/slevelex.res.oracle b/tests/value/oracle_equalities/slevelex.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/small_conditionals.res.oracle b/tests/value/oracle_equalities/small_conditionals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/sort4.0.res.oracle b/tests/value/oracle_equalities/sort4.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/sort4.1.res.oracle b/tests/value/oracle_equalities/sort4.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/sort4.2.res.oracle b/tests/value/oracle_equalities/sort4.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/split_return.0.res.oracle b/tests/value/oracle_equalities/split_return.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/split_return.1.res.oracle b/tests/value/oracle_equalities/split_return.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/split_return.2.res.oracle b/tests/value/oracle_equalities/split_return.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/split_return.3.res.oracle b/tests/value/oracle_equalities/split_return.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/split_return.4.res.oracle b/tests/value/oracle_equalities/split_return.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/statement_contract.res.oracle b/tests/value/oracle_equalities/statement_contract.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/static.res.oracle b/tests/value/oracle_equalities/static.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/strange.res.oracle b/tests/value/oracle_equalities/strange.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/strings.res.oracle b/tests/value/oracle_equalities/strings.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/strings_cond.res.oracle b/tests/value/oracle_equalities/strings_cond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct.res.oracle b/tests/value/oracle_equalities/struct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct2.res.oracle b/tests/value/oracle_equalities/struct2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..61281ee76d0343a86e10d8bc79ed11be6a380d1a
--- /dev/null
+++ b/tests/value/oracle_equalities/struct2.res.oracle
@@ -0,0 +1,30 @@
+55a56,57
+> [kernel] tests/value/struct2.i:78: Warning:
+> all target addresses were invalid. This path is assumed to be dead.
+59,60d60
+< accessing out of bounds index. assert 0 ≤ (int)(tab2[i] + j);
+< [eva:alarm] tests/value/struct2.i:82: Warning:
+83,84d82
+< accessing out of bounds index. assert (int)(i + j) < 2;
+< [eva:alarm] tests/value/struct2.i:185: Warning:
+106c104
+< [scope:rm_asserts] removing 2 assertion(s)
+---
+> [scope:rm_asserts] removing 1 assertion(s)
+143,145c141,143
+< tab3[0..1] ∈ [--..--]
+< tab4[0] ∈ {0; 2}
+< [1] ∈ {0}
+---
+> tab3[0] ∈ {0; 1}
+> [1] ∈ [--..--]
+> tab4[0..1] ∈ {0}
+148c146,147
+< tab6[0..1] ∈ {0; 2}
+---
+> tab6[0] ∈ {0}
+> [1] ∈ {2}
+219c218
+< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
+---
+> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
diff --git a/tests/value/oracle_equalities/struct3.res.oracle b/tests/value/oracle_equalities/struct3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct_array.res.oracle b/tests/value/oracle_equalities/struct_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct_call.0.res.oracle b/tests/value/oracle_equalities/struct_call.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct_call.1.res.oracle b/tests/value/oracle_equalities/struct_call.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct_deps.res.oracle b/tests/value/oracle_equalities/struct_deps.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct_incl.res.oracle b/tests/value/oracle_equalities/struct_incl.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/struct_p_call.res.oracle b/tests/value/oracle_equalities/struct_p_call.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/strucval.res.oracle b/tests/value/oracle_equalities/strucval.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/subset.res.oracle b/tests/value/oracle_equalities/subset.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/summary.0.res.oracle b/tests/value/oracle_equalities/summary.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/summary.1.res.oracle b/tests/value/oracle_equalities/summary.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/summary.2.res.oracle b/tests/value/oracle_equalities/summary.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/summary.3.res.oracle b/tests/value/oracle_equalities/summary.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/summary.4.res.oracle b/tests/value/oracle_equalities/summary.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/switch.0.res.oracle b/tests/value/oracle_equalities/switch.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/switch.1.res.oracle b/tests/value/oracle_equalities/switch.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/switch2.res.oracle b/tests/value/oracle_equalities/switch2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/switch_cast.res.oracle b/tests/value/oracle_equalities/switch_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/symbolic_locs.res.oracle b/tests/value/oracle_equalities/symbolic_locs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/tab.res.oracle b/tests/value/oracle_equalities/tab.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/tab1.res.oracle b/tests/value/oracle_equalities/tab1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/termination.res.oracle b/tests/value/oracle_equalities/termination.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/test.0.res.oracle b/tests/value/oracle_equalities/test.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/test.1.res.oracle b/tests/value/oracle_equalities/test.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/test_arith.res.oracle b/tests/value/oracle_equalities/test_arith.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/threat_array.res.oracle b/tests/value/oracle_equalities/threat_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/threat_if.res.oracle b/tests/value/oracle_equalities/threat_if.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/threat_redundant.res.oracle b/tests/value/oracle_equalities/threat_redundant.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/tricky_logic.res.oracle b/tests/value/oracle_equalities/tricky_logic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/typedef_function.res.oracle b/tests/value/oracle_equalities/typedef_function.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/typeof.res.oracle b/tests/value/oracle_equalities/typeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ulongvslonglong.0.res.oracle b/tests/value/oracle_equalities/ulongvslonglong.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/ulongvslonglong.1.res.oracle b/tests/value/oracle_equalities/ulongvslonglong.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/undef_behavior_bts1059.res.oracle b/tests/value/oracle_equalities/undef_behavior_bts1059.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/undef_fct.res.oracle b/tests/value/oracle_equalities/undef_fct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/undefined_sequence.0.res.oracle b/tests/value/oracle_equalities/undefined_sequence.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/undefined_sequence.1.res.oracle b/tests/value/oracle_equalities/undefined_sequence.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/undefined_sequence2.res.oracle b/tests/value/oracle_equalities/undefined_sequence2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/uninit.res.oracle b/tests/value/oracle_equalities/uninit.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/uninit_callstack.res.oracle b/tests/value/oracle_equalities/uninit_callstack.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/uninitialized_gnubody.res.oracle b/tests/value/oracle_equalities/uninitialized_gnubody.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/unknown_sizeof.0.res.oracle b/tests/value/oracle_equalities/unknown_sizeof.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/unknown_sizeof.1.res.oracle b/tests/value/oracle_equalities/unknown_sizeof.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/unop.res.oracle b/tests/value/oracle_equalities/unop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/unroll.res.oracle b/tests/value/oracle_equalities/unroll.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/unroll_simple.res.oracle b/tests/value/oracle_equalities/unroll_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/unsigned_overflow.res.oracle b/tests/value/oracle_equalities/unsigned_overflow.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/use_spec.0.res.oracle b/tests/value/oracle_equalities/use_spec.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/use_spec.1.res.oracle b/tests/value/oracle_equalities/use_spec.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/user_assertion_uninit_var.res.oracle b/tests/value/oracle_equalities/user_assertion_uninit_var.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/usp.res.oracle b/tests/value/oracle_equalities/usp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/va_list.0.res.oracle b/tests/value/oracle_equalities/va_list.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/va_list.1.res.oracle b/tests/value/oracle_equalities/va_list.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/va_list2.0.res.oracle b/tests/value/oracle_equalities/va_list2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/va_list2.1.res.oracle b/tests/value/oracle_equalities/va_list2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val6.0.res.oracle b/tests/value/oracle_equalities/val6.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val6.1.res.oracle b/tests/value/oracle_equalities/val6.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val_if.0.res.oracle b/tests/value/oracle_equalities/val_if.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val_if.1.res.oracle b/tests/value/oracle_equalities/val_if.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val_if.2.res.oracle b/tests/value/oracle_equalities/val_if.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val_ptr.0.res.oracle b/tests/value/oracle_equalities/val_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val_ptr.1.res.oracle b/tests/value/oracle_equalities/val_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val_ptr.2.res.oracle b/tests/value/oracle_equalities/val_ptr.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/val_ptr.3.res.oracle b/tests/value/oracle_equalities/val_ptr.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/video_detect.res.oracle b/tests/value/oracle_equalities/video_detect.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/volatile.res.oracle b/tests/value/oracle_equalities/volatile.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/volatile2.res.oracle b/tests/value/oracle_equalities/volatile2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/volatilestruct.res.oracle b/tests/value/oracle_equalities/volatilestruct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/wide_string.res.oracle b/tests/value/oracle_equalities/wide_string.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/widen_non_constant.res.oracle b/tests/value/oracle_equalities/widen_non_constant.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/widen_on_non_monotonic.res.oracle b/tests/value/oracle_equalities/widen_on_non_monotonic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/widen_overflow.res.oracle b/tests/value/oracle_equalities/widen_overflow.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/widening_thresholds.res.oracle b/tests/value/oracle_equalities/widening_thresholds.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/with_comment.res.oracle b/tests/value/oracle_equalities/with_comment.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_equalities/zerolengtharrays.res.oracle b/tests/value/oracle_equalities/zerolengtharrays.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391