diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,10 @@
 
 # Release Notes
 
+## 4.2.0
+
+This release removes support for SMT-LIB 1.x in order to be compatible with Z3 4.6.
+
 ## 4.1.2
 
 This minor release extends the supported quantifiers API, and adds
diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs
--- a/src/Z3/Base.hs
+++ b/src/Z3/Base.hs
@@ -2244,7 +2244,6 @@
 data ASTPrintMode
   = Z3_PRINT_SMTLIB_FULL
   | Z3_PRINT_LOW_LEVEL
-  | Z3_PRINT_SMTLIB_COMPLIANT
   | Z3_PRINT_SMTLIB2_COMPLIANT
 
 -- | Set the pretty-printing mode for converting ASTs to strings.
@@ -2255,8 +2254,6 @@
          z3_set_ast_print_mode ctxPtr z3_print_smtlib_full
        Z3_PRINT_LOW_LEVEL ->
          z3_set_ast_print_mode ctxPtr z3_print_low_level
-       Z3_PRINT_SMTLIB_COMPLIANT ->
-         z3_set_ast_print_mode ctxPtr z3_print_smtlib_compliant
        Z3_PRINT_SMTLIB2_COMPLIANT ->
          z3_set_ast_print_mode ctxPtr z3_print_smtlib2_compliant
 
diff --git a/src/Z3/Base/C.hsc b/src/Z3/Base/C.hsc
--- a/src/Z3/Base/C.hsc
+++ b/src/Z3/Base/C.hsc
@@ -103,8 +103,6 @@
 z3_print_smtlib_full = #const Z3_PRINT_SMTLIB_FULL
 z3_print_low_level :: Z3_ast_print_mode
 z3_print_low_level = #const Z3_PRINT_LOW_LEVEL
-z3_print_smtlib_compliant :: Z3_ast_print_mode
-z3_print_smtlib_compliant = #const Z3_PRINT_SMTLIB_COMPLIANT
 z3_print_smtlib2_compliant :: Z3_ast_print_mode
 z3_print_smtlib2_compliant = #const Z3_PRINT_SMTLIB2_COMPLIANT
 
diff --git a/z3.cabal b/z3.cabal
--- a/z3.cabal
+++ b/z3.cabal
@@ -1,5 +1,5 @@
 Name:                z3
-Version:             4.1.2
+Version:             4.2.0
 Synopsis:            Bindings for the Z3 Theorem Prover
 Description:
     Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).
@@ -29,7 +29,7 @@
 Author:              Iago Abal <mail@iagoabal.eu>,
                      David Castro <david.castro.dcp@gmail.com>
 Maintainer:          Iago Abal <mail@iagoabal.eu>
-Copyright:           2012-2017, Iago Abal, David Castro
+Copyright:           2012-2018, Iago Abal, David Castro
 Category:            Math, SMT, Theorem Provers, Formal Methods, Bit vectors
 Build-type:          Simple
 Cabal-version:       >= 1.8