diff --git a/Makefile b/Makefile
index 2f39dd618b..88fd42ec69 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@ ECARGS    ?=
 ECTOUT    ?= 10
 ECJOBS    ?= 0
 ECEXTRA   ?= --report=report.log
-ECPROVERS ?= Alt-Ergo Z3 CVC4
+ECPROVERS ?= Alt-Ergo@2.4 Z3@4.8 CVC4@1.8
 CHECKPY   ?=
 CHECK     := $(CHECKPY) scripts/testing/runtest
 CHECK     += --bin=./ec.native --bin-args="$(ECARGS)"
diff --git a/src/ec.ml b/src/ec.ml
index 4a76f5eb94..8d8e28a4df 100644
--- a/src/ec.ml
+++ b/src/ec.ml
@@ -72,7 +72,7 @@ let print_config config =
       let fullname =
         Printf.sprintf "%s@%s"
           prover.EcProvers.pr_name
-          prover.EcProvers.pr_version in
+          (EcProvers.Version.to_string prover.EcProvers.pr_version) in
 
       match prover.EcProvers.pr_evicted with
       | None -> fullname
diff --git a/src/ecProvers.ml b/src/ecProvers.ml
index 5bea4fa487..2f8005aab5 100644
--- a/src/ecProvers.ml
+++ b/src/ecProvers.ml
@@ -70,7 +70,7 @@ let test_if_evict_prover test (name, version) =
   let evict =
     match test.pe_test with
     | `ByVersion (tname, (trel, tversion)) when name = tname -> begin
-        let cmp = VP.compare (VP.parse version) tversion in
+        let cmp = VP.compare version tversion in
         match trel with
         | `Eq -> cmp =  0
         | `Lt -> cmp <  0
@@ -107,7 +107,7 @@ let evictions : prover_eviction_test list = [
 (* -------------------------------------------------------------------- *)
 type prover = {
   pr_name    : string;
-  pr_version : string;
+  pr_version : Version.version;
   pr_evicted : (prover_eviction * bool) option;
 }
 
@@ -155,7 +155,7 @@ end = struct
 
         { pr_prover  =
             { pr_name    = name;
-              pr_version = version;
+              pr_version = Version.parse version;
               pr_evicted = None; };
           pr_config  = config;
           pr_driver  = driver; }
@@ -212,24 +212,65 @@ exception UnknownProver of string
 
 type parsed_pname = {
   prn_name     : string;
+  prn_version  : Version.version option;
   prn_ovrevict : bool;
 }
 
 let parse_prover_name name =
+  let name, version =
+    if String.contains name '@' then
+      let index   = String.index name '@' in
+      let name    = String.sub name 0 index
+      and version = String.sub name (index+1) (String.length name - (index+1)) in
+      (name, Some version)
+    else
+      (name, None) in
+
+  let version = omap Version.parse version in
+
   if   name <> "" && name.[0] = '!'
   then { prn_name     = String.sub name 1 (String.length name - 1);
+         prn_version  = version;
          prn_ovrevict = true; }
-  else { prn_name = name; prn_ovrevict = false; }
+  else { prn_name     = name;
+         prn_version  = version;
+         prn_ovrevict = false; }
 
-let get_prover name =
-  let name = parse_prover_name name in
+let get_prover (rawname : string) =
+  let name = parse_prover_name rawname in
 
   let test p =
        p.pr_prover.pr_name = name.prn_name
     && (name.prn_ovrevict || not (is_evicted p.pr_prover)) in
 
-  try  List.find test (Config.provers ())
-  with Not_found -> raise (UnknownProver name.prn_name)
+  let provers = List.filter test (Config.provers ()) in
+
+  let provers = List.sort (fun p1 p2 ->
+      let v1 = p1.pr_prover.pr_version in
+      let v2 = p2.pr_prover.pr_version in
+      Version.compare v1 v2
+    ) provers
+  in
+
+  let exception CannotFindProver in
+
+  try
+    match name.prn_version with
+    | None ->
+        oget ~exn:CannotFindProver (List.Exceptionless.hd (List.rev provers))
+
+    | Some version -> begin
+        try
+          List.find
+            (fun p ->
+               Version.compare version p.pr_prover.pr_version <= 0)
+          provers
+
+        with Not_found -> raise CannotFindProver
+      end
+
+  with CannotFindProver ->
+    raise (UnknownProver rawname)
 
 let is_prover_known name =
   try ignore (get_prover name); true with UnknownProver _ -> false
diff --git a/src/ecProvers.mli b/src/ecProvers.mli
index d8f2116698..70b345f77b 100644
--- a/src/ecProvers.mli
+++ b/src/ecProvers.mli
@@ -15,6 +15,13 @@ module Hints : sig
   val mem : path -> hints -> bool
 end
 
+(* -------------------------------------------------------------------- *)
+module Version : sig
+  type version
+
+  val to_string : version -> string
+end
+
 (* -------------------------------------------------------------------- *)
 type prover_eviction = [
   | `Inconsistent
@@ -22,7 +29,7 @@ type prover_eviction = [
 
 type prover = {
   pr_name    : string;
-  pr_version : string;
+  pr_version : Version.version;
   pr_evicted : (prover_eviction * bool) option;
 }
 
@@ -51,6 +58,7 @@ val known : evicted:bool -> prover list
 (* -------------------------------------------------------------------- *)
 type parsed_pname = {
   prn_name     : string;
+  prn_version  : Version.version option;
   prn_ovrevict : bool;
 }