Merge branch 'fix/virgile/opam-descr' into 'stable/zinc'

update opam description for Aoraï

See merge request frama-c/frama-c!4820

opam

@@ -10,7 +10,7 @@ Thanks to this approach, Frama-C provides sophisticated tools, including:
 - an analyzer based on abstract interpretation (Eva plug-in);
 - a program proof framework based on weakest precondition calculus (WP plug-in);
 - a program slicer (Slicing plug-in);
-- a tool for verification of temporal (LTL) properties (Aoraï plug-in);
+- a tool for verification of automata-based properties (Aoraï plug-in);
 - a runtime verification tool (E-ACSL plug-in);
 - several tools for code base exploration and dependency analysis
   (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.).
@@ -80,7 +80,7 @@ dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
 doc: "https://frama-c.com/download/user-manual-30.0-beta-Zinc.pdf"
 bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
 tags: [
-  "deductive"
+  "deductive verification"
   "program verification"
   "formal specification"
   "automated theorem prover"
@@ -177,6 +177,7 @@ post-messages: [
 Recommended provers are:
 - Alt-Ergo (https://alt-ergo.ocamlpro.com)
 - CVC4     (https://cvc4.github.io)
+- CVC5     (https://cvc5.github.io)
 - Z3       (https://github.com/Z3Prover/z3)
 Use 'why3 config detect' to configure new provers.
  " { success }