[wp] test with cvc4

src/plugins/wp/tests/wp_plugin/cvc4_ce.i

+/* run.config_qualif
+   OPT: -wp -wp-counter-examples -wp-prover cvc4 -wp-status
+ */
+
+//@ check lemma wrong: \forall integer x; \abs(x) == x;
+
+//@ ensures \result == \abs(x); assigns \nothing;
+int wrong(int x) { return x; }

src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing cvc4_ce.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal wrong_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Check Lemma 'wrong':
+Prove: IAbs.abs(x) = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function wrong
+------------------------------------------------------------
+
+Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Assume { Type: is_sint32(wrong_0). }
+Prove: IAbs.abs(wrong_0) = wrong_0.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'wrong':
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing cvc4_ce.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal wrong_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Unsuccess] typed_check_lemma_wrong (CVC4) (No Cache) (Model)
+[wp] [Unsuccess] typed_wrong_ensures (CVC4) (No Cache) (Model)
+[wp] [Valid] typed_wrong_assigns (Qed)
+[wp] Proved goals:    3 / 5
+  Terminating:     1
+  Unreachable:     1
+  Qed:             1
+  Unsuccess:       2
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Check Lemma 'wrong':
+Assume { Probe x = x. }
+Prove: IAbs.abs(x) = x.
+Prover CVC4 returns Unsuccess (Model)
+Model x = -1
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function wrong
+------------------------------------------------------------
+
+Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Assume { Type: is_sint32(wrong_0). Probe x = wrong_0. }
+Prove: IAbs.abs(wrong_0) = wrong_0.
+Prover CVC4 returns Unsuccess (Model)
+Model x = -1
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        -        1       0.0%
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  wrong                     1        -        2      50.0%
+------------------------------------------------------------