diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
index 046a6a7f967f4de51161c85675714c523fe96060..888e5f6719ee01a513e3c06aaa09b8e30ed6c5bd 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
@@ -3,7 +3,6 @@
 [eva:alarm] tests/arith/quantif.i:15: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/quantif.i:15: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:20: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/quantif.i:24: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/quantif.i:24: Warning: assertion got status unknown.
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index 21fd920919affc8afd1710f3d43042b975c924b3..770361f547028d044dea20eeb4bd77a6108ac9bb 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -23,6 +23,8 @@
 [eva] tests/builtins/strchr.c:88: Call to builtin strchr
 [eva] tests/builtins/strchr.c:88: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva] tests/builtins/strchr.c:88: Frama_C_show_each_mystrchr: {3}
 [eva] tests/builtins/strchr.c:89: assertion got status valid.
 [eva] tests/builtins/strchr.c:92: Call to builtin strchr
diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index fc9107a81028a0d522e0ae1ecb02cfdafa64c96b..e39d01ba5bf5415cbb065c34c0e0af0a79d49307 100644
--- a/tests/libc/oracle/stdlib_c_env.res.oracle
+++ b/tests/libc/oracle/stdlib_c_env.res.oracle
@@ -9,6 +9,8 @@
 [eva] share/libc/stdlib.c:114: Call to builtin strchr
 [eva] share/libc/stdlib.c:114: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva] share/libc/stdlib.c:115: 
   assertion 'string_contains_separator' got status valid.
 [eva] share/libc/stdlib.c:116: assertion 'name_is_not_empty' got status valid.
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 033c83c6b476d861790f1c98a4074809e81bc6e2..401829973b44023601fe892716db53d08870ea00 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -668,6 +668,8 @@
   function strchr, behavior found: postcondition 'result_in_length' got status valid.
 [eva] share/libc/string.h:164: 
   function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva:alarm] share/libc/string.h:165: Warning: 
   function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
 [eva] share/libc/string.h:171: 
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index d2f546a60acf81596b0b9778e9f97cfd59ddedba..4e1e5145535fa6ef9dd6ed43f042e6125df52320 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -288,6 +288,8 @@
   function strchr, behavior found: postcondition 'result_in_length' got status valid.
 [eva] share/libc/string.h:164: 
   function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva:alarm] share/libc/string.h:165: Warning: 
   function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
 [eva] share/libc/string.h:171: 
diff --git a/tests/libc/oracle/string_c_strchr.res.oracle b/tests/libc/oracle/string_c_strchr.res.oracle
index 965af4a3862fe7990d7ca5c2fa9ece0a8c3fc0f8..d389a3cf5615c82c1b364e246fbcfeded5ef7fca 100644
--- a/tests/libc/oracle/string_c_strchr.res.oracle
+++ b/tests/libc/oracle/string_c_strchr.res.oracle
@@ -67,6 +67,8 @@
   function strchr, behavior found: postcondition 'result_in_length' got status valid.
 [eva] share/libc/string.h:164: 
   function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva:alarm] share/libc/string.h:165: Warning: 
   function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
 [eva] Recording results for strchr
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 5e1e94a0719c6c96067d3788889d10788b9d8c45..fd2eaee19bf54f636ccc83358a1c4dc259534597 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -143,12 +143,8 @@
 [eva] tests/libc/string_h.c:75: 
   function strtok: precondition 'valid_string_delim' got status valid.
 [eva:alarm] tests/libc/string_h.c:75: Warning: 
-  function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:75: 
-  Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+  function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
 [eva] Done for function strtok
-[eva:alarm] tests/libc/string_h.c:76: Warning: 
-  assertion 'unreachable_if_precise' got status invalid (stopping propagation).
 [eva] Recording results for test_strtok
 [eva] Done for function test_strtok
 [eva] computing for function test_strtok_r <- main.
@@ -232,12 +228,8 @@
 [eva] tests/libc/string_h.c:105: 
   function strtok_r: precondition 'valid_saveptr' got status valid.
 [eva:alarm] tests/libc/string_h.c:105: Warning: 
-  function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:105: 
-  Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+  function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
 [eva] Done for function strtok_r
-[eva:alarm] tests/libc/string_h.c:106: Warning: 
-  assertion 'unreachable_if_precise' got status invalid (stopping propagation).
 [eva] Recording results for test_strtok_r
 [eva] Done for function test_strtok_r
 [eva] computing for function strdup <- main.
@@ -333,6 +325,8 @@
 [eva] tests/libc/string_h.c:154: Call to builtin strchr
 [eva] tests/libc/string_h.c:154: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva] computing for function strchrnul <- main.
   Called from tests/libc/string_h.c:155.
 [eva] using specification for function strchrnul
diff --git a/tests/value/oracle/annot_valid.res.oracle b/tests/value/oracle/annot_valid.res.oracle
index 88f57174bb9ee088a5e1aff1fccb060ef9e86128..557e8ca2b58d364e59f43e41c027e413c56505f4 100644
--- a/tests/value/oracle/annot_valid.res.oracle
+++ b/tests/value/oracle/annot_valid.res.oracle
@@ -17,7 +17,7 @@
 [eva:alarm] tests/value/annot_valid.i:29: Warning: assertion got status unknown.
 [eva:alarm] tests/value/annot_valid.i:32: Warning: assertion got status unknown.
 [eva:alarm] tests/value/annot_valid.i:35: Warning: assertion got status unknown.
-[eva:alarm] tests/value/annot_valid.i:38: Warning: assertion got status unknown.
+[eva] tests/value/annot_valid.i:38: assertion got status valid.
 [eva] tests/value/annot_valid.i:41: assertion got status valid.
 [eva:alarm] tests/value/annot_valid.i:44: Warning: 
   assertion got status invalid (stopping propagation).