diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 5ab56d1c7..8f75e97ed 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 5, 1, 0)
+    set_version(4, 6, 1, 0)
     add_lib('util', [])
     add_lib('lp', ['util'], 'util/lp')
     add_lib('polynomial', ['util'], 'math/polynomial')
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 914cee615..ac23d1dbc 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3320,160 +3320,10 @@ namespace Microsoft.Z3
         #endregion
 
         #region SMT Files & Strings
-        /// <summary>
-        /// Convert a benchmark into an SMT-LIB formatted string.
-        /// </summary>
-        /// <param name="name">Name of the benchmark. The argument is optional.</param>
-        /// <param name="logic">The benchmark logic. </param>
-        /// <param name="status">The status string (sat, unsat, or unknown)</param>
-        /// <param name="attributes">Other attributes, such as source, difficulty or category.</param>
-        /// <param name="assumptions">Auxiliary assumptions.</param>
-        /// <param name="formula">Formula to be checked for consistency in conjunction with assumptions.</param>
-        /// <returns>A string representation of the benchmark.</returns>
-        public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
-                                           BoolExpr[] assumptions, BoolExpr formula)
-        {
-            Contract.Requires(assumptions != null);
-            Contract.Requires(formula != null);
-            Contract.Ensures(Contract.Result<string>() != null);
-
-            return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
-                                            (uint)assumptions.Length, AST.ArrayToNative(assumptions),
-                                            formula.NativeObject);
-        }
-
-        /// <summary>
-        /// Parse the given string using the SMT-LIB parser.
-        /// </summary>
-        /// <remarks>
-        /// The symbol table of the parser can be initialized using the given sorts and declarations.
-        /// The symbols in the arrays <paramref name="sortNames"/> and <paramref name="declNames"/>
-        /// don't need to match the names of the sorts and declarations in the arrays <paramref name="sorts"/>
-        /// and <paramref name="decls"/>. This is a useful feature since we can use arbitrary names to
-        /// reference sorts and declarations.
-        /// </remarks>
-        public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
-        {
-            uint csn = Symbol.ArrayLength(sortNames);
-            uint cs = Sort.ArrayLength(sorts);
-            uint cdn = Symbol.ArrayLength(declNames);
-            uint cd = AST.ArrayLength(decls);
-            if (csn != cs || cdn != cd)
-                throw new Z3Exception("Argument size mismatch");
-            Native.Z3_parse_smtlib_string(nCtx, str,
-                AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
-                AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
-        }
-
-        /// <summary>
-        /// Parse the given file using the SMT-LIB parser.
-        /// </summary>
-        /// <seealso cref="ParseSMTLIBString"/>
-        public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
-        {
-            uint csn = Symbol.ArrayLength(sortNames);
-            uint cs = Sort.ArrayLength(sorts);
-            uint cdn = Symbol.ArrayLength(declNames);
-            uint cd = AST.ArrayLength(decls);
-            if (csn != cs || cdn != cd)
-                throw new Z3Exception("Argument size mismatch");
-            Native.Z3_parse_smtlib_file(nCtx, fileName,
-                AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
-                AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
-        }
-
-        /// <summary>
-        /// The number of SMTLIB formulas parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
-
-        /// <summary>
-        /// The formulas parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public BoolExpr[] SMTLIBFormulas
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
-
-                uint n = NumSMTLIBFormulas;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// The number of SMTLIB assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
-
-        /// <summary>
-        /// The assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public BoolExpr[] SMTLIBAssumptions
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
-
-                uint n = NumSMTLIBAssumptions;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// The number of SMTLIB declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
-
-        /// <summary>
-        /// The declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public FuncDecl[] SMTLIBDecls
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
-                uint n = NumSMTLIBDecls;
-                FuncDecl[] res = new FuncDecl[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// The number of SMTLIB sorts parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
-
-        /// <summary>
-        /// The declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
-        /// </summary>
-        public Sort[] SMTLIBSorts
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<Sort[]>() != null);
-
-                uint n = NumSMTLIBSorts;
-                Sort[] res = new Sort[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
-                return res;
-            }
-        }
 
         /// <summary>
         /// Parse the given string using the SMT-LIB2 parser.
         /// </summary>
-        /// <seealso cref="ParseSMTLIBString"/>
         /// <returns>A conjunction of assertions in the scope (up to push/pop) at the end of the string.</returns>
         public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
         {
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 76303d670..3458f4d97 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2540,147 +2540,8 @@ public class Context implements AutoCloseable {
                 AST.arrayToNative(assumptions), formula.getNativeObject());
     }
 
-    /**
-     * Parse the given string using the SMT-LIB parser.
-     * Remarks:  The symbol
-     * table of the parser can be initialized using the given sorts and
-     * declarations. The symbols in the arrays {@code sortNames} and
-     * {@code declNames} don't need to match the names of the sorts
-     * and declarations in the arrays {@code sorts} and {@code decls}. This is a useful feature since we can use arbitrary names
-     * to reference sorts and declarations. 
-     **/
-    public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
-            Symbol[] declNames, FuncDecl[] decls)
-    {
-        int csn = Symbol.arrayLength(sortNames);
-        int cs = Sort.arrayLength(sorts);
-        int cdn = Symbol.arrayLength(declNames);
-        int cd = AST.arrayLength(decls);
-        if (csn != cs || cdn != cd)
-            throw new Z3Exception("Argument size mismatch");
-        Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
-                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
-                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
-                AST.arrayToNative(decls));
-    }
-
-    /**
-     * Parse the given file using the SMT-LIB parser. 
-     * @see #parseSMTLIBString
-     **/
-    public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
-            Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
-           
-    {
-        int csn = Symbol.arrayLength(sortNames);
-        int cs = Sort.arrayLength(sorts);
-        int cdn = Symbol.arrayLength(declNames);
-        int cd = AST.arrayLength(decls);
-        if (csn != cs || cdn != cd)
-            throw new Z3Exception("Argument size mismatch");
-        Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
-                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
-                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
-                AST.arrayToNative(decls));
-    }
-
-    /**
-     * The number of SMTLIB formulas parsed by the last call to
-     * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
-     **/
-    public int getNumSMTLIBFormulas()
-    {
-        return Native.getSmtlibNumFormulas(nCtx());
-    }
-
-    /**
-     * The formulas parsed by the last call to {@code ParseSMTLIBString} or
-     * {@code ParseSMTLIBFile}.
-     **/
-    public BoolExpr[] getSMTLIBFormulas()
-    {
-
-        int n = getNumSMTLIBFormulas();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = (BoolExpr) Expr.create(this,
-                    Native.getSmtlibFormula(nCtx(), i));
-        return res;
-    }
-
-    /**
-     * The number of SMTLIB assumptions parsed by the last call to
-     * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
-     **/
-    public int getNumSMTLIBAssumptions()
-    {
-        return Native.getSmtlibNumAssumptions(nCtx());
-    }
-
-    /**
-     * The assumptions parsed by the last call to {@code ParseSMTLIBString}
-     * or {@code ParseSMTLIBFile}.
-     **/
-    public BoolExpr[] getSMTLIBAssumptions()
-    {
-
-        int n = getNumSMTLIBAssumptions();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = (BoolExpr) Expr.create(this,
-                    Native.getSmtlibAssumption(nCtx(), i));
-        return res;
-    }
-
-    /**
-     * The number of SMTLIB declarations parsed by the last call to
-     * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
-     **/
-    public int getNumSMTLIBDecls()
-    {
-        return Native.getSmtlibNumDecls(nCtx());
-    }
-
-    /**
-     * The declarations parsed by the last call to
-     * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
-     **/
-    public FuncDecl[] getSMTLIBDecls()
-    {
-
-        int n = getNumSMTLIBDecls();
-        FuncDecl[] res = new FuncDecl[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
-        return res;
-    }
-
-    /**
-     * The number of SMTLIB sorts parsed by the last call to
-     * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
-     **/
-    public int getNumSMTLIBSorts()
-    {
-        return Native.getSmtlibNumSorts(nCtx());
-    }
-
-    /**
-     * The declarations parsed by the last call to
-     * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}.
-     **/
-    public Sort[] getSMTLIBSorts()
-    {
-
-        int n = getNumSMTLIBSorts();
-        Sort[] res = new Sort[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
-        return res;
-    }
-
     /**
      * Parse the given string using the SMT-LIB2 parser. 
-     * @see #parseSMTLIBString
      * 
      * @return A conjunction of assertions in the scope (up to push/pop) at the
      *         end of the string.