diff --git a/Makefile.in b/Makefile.in
index 9220dd43f7b36c58eceff99dd41491c72dc95580..b2296d2ba7b6388bf6e9415c6379232cdcae176d 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -133,8 +133,8 @@ LIBGENERATED = src/util/config.ml \
 	       src/parser/parser.mli src/parser/parser.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
 	       src/driver/driver_lexer.ml \
-               src/driver/parse_cvc4_z3_model_parser.mli src/driver/parse_cvc4_z3_model_parser.ml \
-               src/driver/parse_cvc4_z3_model_lexer.ml \
+               src/driver/parse_smtv2_model_parser.mli src/driver/parse_smtv2_model_parser.ml \
+               src/driver/parse_smtv2_model_lexer.ml \
 	       src/session/compress.ml src/session/xml.ml \
 	       src/session/strategy_parser.ml \
 	       lib/ocaml/why3__BigInt_compat.ml
@@ -149,7 +149,7 @@ LIB_CORE = ident ty term pattern decl theory \
 
 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     whyconf autodetection \
-             parse_cvc4_z3_model_parser parse_cvc4_z3_model_lexer parse_cvc4_z3_model
+             parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
 
 LIB_MLW = ity expr dexpr
 
diff --git a/drivers/cvc4_15.drv b/drivers/cvc4_15.drv
index b6ef60d181bf1a8711cfbc72688e05f2c4783280..bb7c194d79fb7bbf6b2454daa0feee254581fae5 100644
--- a/drivers/cvc4_15.drv
+++ b/drivers/cvc4_15.drv
@@ -24,7 +24,7 @@ transformation "introduce_premises"
 transformation "intro_projections_counterexmp"
 
 (* Counterexamples: set model parser *)
-model_parser "cvc4_z3"
+model_parser "smtv2"
 
 import "smt-libv2.drv"
 import "smt-libv2-bv.gen"
diff --git a/drivers/cvc4_bare.drv b/drivers/cvc4_bare.drv
index 097acd7da59105a5e0ae1189f6db35168cc99f3e..4f9292979a2142076dfd8982bcac013ad8795b55 100644
--- a/drivers/cvc4_bare.drv
+++ b/drivers/cvc4_bare.drv
@@ -20,7 +20,7 @@ prelude "(set-option :produce-models true)"
 transformation "introduce_premises"
 
 (* Counterexamples: set model parser *)
-model_parser "cvc4_z3"
+model_parser "smtv2"
 
 import "smt-libv2.drv"
 
diff --git a/drivers/z3_432.drv b/drivers/z3_432.drv
index ee21fc4f564b3ed249e7b62bf4e0dd7e459e9b67..dd9a0cd7f61b14f70aafeb124cc83ab03c1f8f67 100644
--- a/drivers/z3_432.drv
+++ b/drivers/z3_432.drv
@@ -13,7 +13,7 @@ transformation "introduce_premises"
 transformation "intro_projections_counterexmp"
 
 (* Counterexamples: set model parser *)
-model_parser "cvc4_z3"
+model_parser "smtv2"
 
 
 import "smt-libv2.drv"
diff --git a/src/driver/parse_cvc4_z3_model.ml b/src/driver/parse_smtv2_model.ml
similarity index 93%
rename from src/driver/parse_cvc4_z3_model.ml
rename to src/driver/parse_smtv2_model.ml
index 1a26120dc3fff9d370cb7523d81e4e891484ada7..0b3da19b3e2688dff88b14fc6c771806ced41473 100644
--- a/src/driver/parse_cvc4_z3_model.ml
+++ b/src/driver/parse_smtv2_model.ml
@@ -17,7 +17,7 @@ open Term
 open Model_parser
 open Lexing
 
-let debug = Debug.register_info_flag "parse_cvc4_z3_model"
+let debug = Debug.register_info_flag "parse_smtv2_model"
   ~desc:"Print@ debugging@ messages@ about@ parsing@ model@ \
          returned@ from@ cvc4@ or@ z3."
 
@@ -88,14 +88,14 @@ let get_position lexbuf =
 let do_parsing model =
   let lexbuf = Lexing.from_string model in
   try
-    Parse_cvc4_z3_model_parser.output Parse_cvc4_z3_model_lexer.token lexbuf
+    Parse_smtv2_model_parser.output Parse_smtv2_model_lexer.token lexbuf
   with
-  | Parse_cvc4_z3_model_lexer.SyntaxError -> 
+  | Parse_smtv2_model_lexer.SyntaxError -> 
     Warning.emit 
       ~loc:(get_position lexbuf)
       "Error@ during@ lexing@ of@ smtlib@ model:@ unexpected character";
     []
-  | Parse_cvc4_z3_model_parser.Error ->
+  | Parse_smtv2_model_parser.Error ->
     begin
       let loc = get_position lexbuf in
       Warning.emit ~loc:loc "Error@ during@ parsing@ of@ smtlib@ model";
@@ -121,5 +121,5 @@ let parse input printer_mapping =
   | Not_found -> [] 
 
     
-let () = register_model_parser "cvc4_z3" parse
+let () = register_model_parser "smtv2" parse
   ~desc:"Parser@ for@ the@ model@ of@ cv4@ and@ z3."
diff --git a/src/driver/parse_cvc4_z3_model_lexer.mll b/src/driver/parse_smtv2_model_lexer.mll
similarity index 93%
rename from src/driver/parse_cvc4_z3_model_lexer.mll
rename to src/driver/parse_smtv2_model_lexer.mll
index 6d4d4c8f6d78d05ef9014900711cad56bef16375..3a52efb7df9ff1ec71f25fd933428f103f84e1ba 100644
--- a/src/driver/parse_cvc4_z3_model_lexer.mll
+++ b/src/driver/parse_smtv2_model_lexer.mll
@@ -1,5 +1,5 @@
 {
-  open Parse_cvc4_z3_model_parser
+  open Parse_smtv2_model_parser
   exception SyntaxError
 }
 
diff --git a/src/driver/parse_cvc4_z3_model_parser.mly b/src/driver/parse_smtv2_model_parser.mly
similarity index 99%
rename from src/driver/parse_cvc4_z3_model_parser.mly
rename to src/driver/parse_smtv2_model_parser.mly
index c334ed85ba8bdc44d2dcfe61310820a83e6aa6b7..4d92480ea1a1b3cb749fc06d07dce193c2e6d3b8 100644
--- a/src/driver/parse_cvc4_z3_model_parser.mly
+++ b/src/driver/parse_smtv2_model_parser.mly
@@ -104,3 +104,4 @@ array:
 
 array_skipped_part:
 | LPAREN term_list RPAREN {}
+