diff --git a/src/plugins/wp/tests/wp_bts/issue_715_a.i b/src/plugins/wp/tests/wp_bts/issue_715_a.i
new file mode 100644
index 0000000000000000000000000000000000000000..bcadfd9430cafe19ac5a3843d8fc35de91ed4a65
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_715_a.i
@@ -0,0 +1,10 @@
+/*@
+ requires *s >= 0 ;
+*/
+void dummy(int *s);
+
+void foo(void)
+{
+ int p[1] = { 0 };
+ dummy(p);
+}
diff --git a/src/plugins/wp/tests/wp_bts/issue_715_b.i b/src/plugins/wp/tests/wp_bts/issue_715_b.i
new file mode 100644
index 0000000000000000000000000000000000000000..f6f9a524280e52cf28164debe448e82aad2cd517
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_715_b.i
@@ -0,0 +1,12 @@
+//@ predicate isValid(int *s) = \valid(s);
+
+/*@
+ requires isValid(dest);
+ requires dest[0] >= 0;
+*/
+void dummy(int *dest);
+
+void foo(){
+ int p[1] = { 0 } ;
+ dummy(p);
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..77c9d7c737c7e9b2b8c6ab7c2e8893d22a112adb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_a.i:6: Warning:
+ No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function foo
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_bts/issue_715_a.i, line 2) in 'dummy'' in 'foo' at call 'dummy' (file tests/wp_bts/issue_715_a.i, line 9)
+:
+Assume { Type: is_sint32(p). (* Initializer *) Init: p[0] = 0. }
+Prove: 0 <= p.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..13a226ffae85921197d34d1462103e397775d442
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
@@ -0,0 +1,23 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_b.i:9: Warning:
+ No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function foo
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_bts/issue_715_b.i, line 4) in 'dummy'' in 'foo' at call 'dummy' (file tests/wp_bts/issue_715_b.i, line 11)
+:
+Assume { (* Heap *) Have: linked(Malloc_0). }
+Prove: P_isValid(Malloc_0, shift_sint32(global(L_p_28), 0)).
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_bts/issue_715_b.i, line 5) in 'dummy'' in 'foo' at call 'dummy' (file tests/wp_bts/issue_715_b.i, line 11)
+:
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b8a10bc601a0ed497a92146051de9c9f1b09a794
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
@@ -0,0 +1,58 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_a.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_a.i:6: Warning:
+ No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] Failure: Error in why3:anomaly: File "src/plugins/wp/ProverWhy3.ml", line 586, characters 9-15: Assertion failed
+ Raised at file "src/plugins/wp/ProverWhy3.ml", line 586, characters 9-21
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 383, characters 16-41
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 542, characters 10-33
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 578, characters 10-26
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 575, characters 25-51
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 304, characters 27-53
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 542, characters 10-33
+ Called from file "src/libraries/stdlib/extlib.ml", line 343, characters 14-17
+ Re-raised at file "src/libraries/stdlib/extlib.ml", line 343, characters 41-48
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 963, characters 10-44
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 978, characters 17-57
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 1258, characters 19-34
+ Called from file "src/plugins/wp/wpContext.ml", line 136, characters 17-20
+ Re-raised at file "src/plugins/wp/wpContext.ml", line 141, characters 23-32
+ Called from file "src/plugins/wp/ProverWhy3.ml", line 1255, characters 4-1023
+[kernel] Current source was: tests/wp_bts/issue_715_a.i:6
+ The full backtrace is:
+ Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 532, characters 24-31
+ Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1098, characters 17-55
+ Called from file "src/kernel_services/plugin_entry_points/log.ml", line 525, characters 9-23
+ Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 528, characters 9-16
+ Called from file "src/plugins/wp/prover.ml", line 62, characters 2-34
+ Called from file "src/libraries/utils/task.ml", line 93, characters 38-43
+ Called from file "src/libraries/utils/task.ml", line 93, characters 38-43
+ Called from file "src/libraries/utils/task.ml" (inlined), line 98, characters 19-29
+ Called from file "src/libraries/utils/task.ml", line 363, characters 14-36
+ Re-raised at file "src/libraries/utils/task.ml", line 369, characters 6-13
+ Called from file "src/libraries/utils/task.ml", line 463, characters 9-22
+ Called from file "array.ml", line 90, characters 31-48
+ Called from file "src/libraries/utils/task.ml", line 480, characters 4-45
+ Called from file "src/libraries/utils/task.ml", line 344, characters 14-18
+ Called from file "src/plugins/wp/register.ml", line 682, characters 4-35
+ Called from file "src/plugins/wp/register.ml", line 768, characters 8-23
+ Called from file "src/libraries/stdlib/extlib.ml", line 343, characters 14-17
+ Re-raised at file "src/libraries/stdlib/extlib.ml", line 343, characters 41-48
+ Called from file "src/libraries/stdlib/extlib.ml", line 344, characters 2-12
+ Called from file "src/libraries/stdlib/extlib.ml", line 344, characters 2-12
+ Called from file "queue.ml", line 105, characters 6-15
+ Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
+
+ Plug-in wp aborted: internal error.
+ Please report as 'crash' at http://bts.frama-c.com/.
+ Your Frama-C version is 19.0+dev (Potassium).
+ Note that a version and a backtrace alone often do not contain enough
+ information to understand the bug. Guidelines for reporting bugs are at:
+ http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json
new file mode 100644
index 0000000000000000000000000000000000000000..9cdd29b8d198d6480feef63cd60c09af33a7f2ca
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json
@@ -0,0 +1,13 @@
+{ "wp:global": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 1, "unknown": 1 } },
+ "wp:functions": { "foo": { "dummy_requires_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "dummy_requires": { "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fbb80ae85bd0dc403d5cd5beb903bd8589e32f04
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_715_b.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[kernel] tests/wp_bts/issue_715_b.i:9: Warning:
+ No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] Warning: creating session directory `tests/wp_bts/oracle_qualif/issue_715_b.0.session'
+[wp] [Failed] Goal typed_foo_call_dummy_requires
+[wp] [Qed] Goal typed_foo_call_dummy_requires_2 : Valid
+[wp] Proved goals: 1 / 2
+ Qed: 1
+[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_715_b.0.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/issue_715_b.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+foo 1 - 2 50.0%
+-------------------------------------------------------------