diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 4a8fbaa0a..081433f1f 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -7,6 +7,8 @@
 
 open Z3enums
 
+exception Error = Z3native.Exception
+
 (* Some helpers. *)
 let null = Z3native.mk_null()
 let is_null o = (Z3native.is_null o)
@@ -283,7 +285,7 @@ struct
       Z3native.ast_map_to_string (z3obj_gnc x) (z3obj_gno x)
   end
 
-  let get_hash_code ( x : ast ) = Z3native.get_ast_hash (z3obj_gnc x) (z3obj_gno x)
+  let hash ( x : ast ) = Z3native.get_ast_hash (z3obj_gnc x) (z3obj_gno x)
   let get_id ( x : ast ) = Z3native.get_ast_id (z3obj_gnc x) (z3obj_gno x)
   let get_ast_kind ( x : ast ) = (ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc x) (z3obj_gno x)))
     
@@ -304,7 +306,7 @@ struct
   let to_sexpr ( x : ast ) = Z3native.ast_to_string (z3obj_gnc x) (z3obj_gno x)
 
 
-  let ( = ) ( a : ast ) ( b : ast ) = (a == b) ||
+  let equal ( a : ast ) ( b : ast ) = (a == b) ||
     if (z3obj_gnc a) != (z3obj_gnc b) then 
       false 
     else 
@@ -314,8 +316,6 @@ struct
     if (get_id a) < (get_id b) then -1 else
       if (get_id a) > (get_id b) then 1 else
 	0
-	  
-  let ( < ) (a : ast) (b : ast) = (compare a b)
     
   let translate ( x : ast ) ( to_ctx : context ) = 
     if (z3obj_gnc x) == (context_gno to_ctx) then 
@@ -361,7 +361,7 @@ struct
     let f ( e : sort ) = match e with Sort(a) -> (AST.ptr_of_ast a) in 
     Array.of_list (List.map f a)
     
-  let ( = ) : sort -> sort -> bool = fun a b ->
+  let equal : sort -> sort -> bool = fun a b ->
     (a == b) ||
       if (gnc a) != (gnc b) then 
 	false 
@@ -424,7 +424,7 @@ sig
   val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl
   val mk_const_decl_s : context -> string -> Sort.sort -> func_decl
   val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl
-  val ( = ) : func_decl -> func_decl -> bool
+  val equal : func_decl -> func_decl -> bool
   val to_string : func_decl -> string
   val get_id : func_decl -> int
   val get_arity : func_decl -> int
@@ -498,7 +498,7 @@ end = struct
     let get_float ( x : parameter ) = 
       match x with
 	| P_Dbl(x) -> x
-	| _ -> raise (Z3native.Exception "parameter is not a double")
+	| _ -> raise (Z3native.Exception "parameter is not a float")
           
     let get_symbol ( x : parameter ) =
       match x with
@@ -545,7 +545,7 @@ end = struct
     create_pdr ctx prefix [] range
 
 
-  let ( = ) ( a : func_decl ) ( b : func_decl ) = (a == b) ||
+  let equal ( a : func_decl ) ( b : func_decl ) = (a == b) ||
     if (gnc a) != (gnc b) then 
       false 
     else 
@@ -605,12 +605,8 @@ sig
   end
   val add_bool : params -> Symbol.symbol -> bool -> unit
   val add_int : params -> Symbol.symbol -> int -> unit
-  val add_double : params -> Symbol.symbol -> float -> unit
+  val add_float : params -> Symbol.symbol -> float -> unit
   val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
-  val add_s_bool : params -> string -> bool -> unit
-  val add_s_int : params -> string -> int -> unit
-  val add_s_double : params -> string -> float -> unit
-  val add_s_symbol : params -> string -> Symbol.symbol -> unit
   val mk_params : context -> params
   val to_string : params -> string
 end = struct
@@ -650,24 +646,12 @@ end = struct
   let add_int ( x : params )  (name : Symbol.symbol ) ( value : int ) =
     Z3native.params_set_uint (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value
       
-  let add_double ( x : params ) ( name : Symbol.symbol ) ( value : float ) =
+  let add_float ( x : params ) ( name : Symbol.symbol ) ( value : float ) =
     Z3native.params_set_double (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) value
 
   let add_symbol ( x : params ) ( name : Symbol.symbol ) ( value : Symbol.symbol ) =
     Z3native.params_set_symbol (z3obj_gnc x) (z3obj_gno x) (Symbol.gno name) (Symbol.gno value)
 
-  let add_s_bool ( x : params ) ( name : string ) ( value : bool ) =
-    add_bool x (Symbol.mk_string (z3obj_gc x) name) value
-      
-  let add_s_int ( x : params) ( name : string ) ( value : int ) =
-    add_int x (Symbol.mk_string (z3obj_gc x) name) value
-      
-  let add_s_double ( x : params ) ( name : string ) ( value : float ) =
-    add_double x (Symbol.mk_string (z3obj_gc x) name) value
-
-  let add_s_symbol ( x : params ) ( name : string ) ( value : Symbol.symbol ) =
-    add_symbol x (Symbol.mk_string (z3obj_gc x) name) value
-
   let mk_params ( ctx : context ) =
     let res : params = { m_ctx = ctx ;
 			 m_n_obj = null ;
@@ -734,8 +718,6 @@ sig
   val is_xor : expr -> bool
   val is_not : expr -> bool
   val is_implies : expr -> bool
-  val is_label : expr -> bool
-  val is_label_lit : expr -> bool
   val is_oeq : expr -> bool
   val mk_const : context -> Symbol.symbol -> Sort.sort -> expr
   val mk_const_s : context -> string -> Sort.sort -> expr
@@ -857,8 +839,6 @@ end = struct
   let is_xor ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_XOR)
   let is_not ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_NOT)
   let is_implies ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_IMPLIES)
-  let is_label ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL)
-  let is_label_lit ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL_LIT)
   let is_oeq ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_OEQ)
 
   let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) =
@@ -1530,20 +1510,20 @@ struct
 	
     let mk_real2int ( ctx : context ) ( t : expr ) =
       (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (Expr.gno t)))
-  end
 
-  module AlgebraicNumber =
-  struct    
-    let to_upper ( x : expr ) ( precision : int ) =
-      expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision)
-	
-    let to_lower ( x : expr ) precision =
-      expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision)
-	
-    let to_decimal_string ( x : expr ) ( precision : int ) = 
-      Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision	
-
-    let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)      
+    module AlgebraicNumber =
+    struct    
+      let to_upper ( x : expr ) ( precision : int ) =
+	expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_upper (Expr.gnc x) (Expr.gno x) precision)
+	  
+      let to_lower ( x : expr ) precision =
+	expr_of_ptr (Expr.gc x) (Z3native.get_algebraic_number_lower (Expr.gnc x) (Expr.gno x) precision)
+	  
+      let to_decimal_string ( x : expr ) ( precision : int ) = 
+	Z3native.get_numeral_decimal_string (Expr.gnc x) (Expr.gno x) precision	
+	  
+      let to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)      
+    end
   end
 
   let is_int ( x : expr ) =
@@ -2052,13 +2032,11 @@ struct
     let f i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_func_decl (z3obj_gnc x) (z3obj_gno x) i) in
     let g i = func_decl_of_ptr (z3obj_gc x) (Z3native.model_get_const_decl (z3obj_gnc x) (z3obj_gno x) i) in
     (mk_list f n_funcs) @ (mk_list g n_consts)
-      
-  exception ModelEvaluationFailedException of string
-      
+            
   let eval ( x : model ) ( t : expr ) ( completion : bool ) =
     let (r, v) = (Z3native.model_eval (z3obj_gnc x) (z3obj_gno x) (Expr.gno t) completion) in
     if not r then
-      raise (ModelEvaluationFailedException "evaluation failed")
+      None
     else
       expr_of_ptr (z3obj_gc x) v
 
@@ -2353,7 +2331,7 @@ struct
 	if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then
 	  (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i))
 	else 
-	  (Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i))
+	  (Entry.create_sd k (Z3native.stats_get_float_value (z3obj_gnc x) (z3obj_gno x) i))
       ) in
       mk_list f n
 
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 1c4c4e922..570ff8717 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -5,6 +5,11 @@
    @author CM Wintersteiger (cwinter) 2012-12-17
 *)
 
+(** General Z3 exceptions 
+
+    Many functions in this API may throw an exception; if they do, it is this one.*)
+exception Error
+
 (** Context objects.
 
     Most interactions with Z3 are interpreted in some context; many users will only 
@@ -188,7 +193,7 @@ sig
 
   (** The AST's hash code.
      @return A hash code *)
-  val get_hash_code : ast -> int
+  val hash : ast -> int
 
   (** A unique identifier for the AST (unique among all ASTs). *)
   val get_id : ast -> int
@@ -220,15 +225,12 @@ sig
   (** Comparison operator.
      @return True if the two ast's are from the same context 
      and represent the same sort; false otherwise. *)
-  val ( = ) : ast -> ast -> bool
+  val equal : ast -> ast -> bool
 
   (** Object Comparison.
      @return Negative if the first ast should be sorted before the second, positive if after else zero. *)
   val compare : ast -> ast -> int
 
-  (** Operator < *)
-  val ( < ) : ast -> ast -> int
-
   (** Translates (copies) the AST to another context.
      @return A copy of the AST which is associated with the other context.  *)
   val translate : ast -> context -> ast
@@ -263,7 +265,7 @@ sig
   (** Comparison operator.
      @return True if the two sorts are from the same context 
      and represent the same sort; false otherwise. *)
-  val ( = ) : sort -> sort -> bool
+  val equal : sort -> sort -> bool
 
   (** Returns a unique identifier for the sort. *)
   val get_id : sort -> int
@@ -310,7 +312,7 @@ sig
     (** The int value of the parameter.*)
     val get_int : parameter -> int
 
-    (** The double value of the parameter.*)
+    (** The float value of the parameter.*)
     val get_float : parameter -> float
 
     (** The Symbol.Symbol value of the parameter.*)
@@ -351,7 +353,7 @@ sig
 
   (** Comparison operator.
       @return True if a and b are from the same context and represent the same func_decl; false otherwise. *)
-  val ( = ) : func_decl -> func_decl -> bool
+  val equal : func_decl -> func_decl -> bool
 
   (** A string representations of the function declaration. *)
   val to_string : func_decl -> string
@@ -423,23 +425,11 @@ sig
   val add_int : params -> Symbol.symbol -> int -> unit
 
   (** Adds a parameter setting. *)
-  val add_double : params -> Symbol.symbol -> float -> unit
+  val add_float : params -> Symbol.symbol -> float -> unit
 
   (** Adds a parameter setting. *)
   val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
 
-  (** Adds a parameter setting. *)
-  val add_s_bool : params -> string -> bool -> unit
-
-  (** Adds a parameter setting. *)
-  val add_s_int : params -> string -> int -> unit
-
-  (** Adds a parameter setting. *)
-  val add_s_double : params -> string -> float -> unit
-
-  (** Adds a parameter setting. *)
-  val add_s_symbol : params -> string -> Symbol.symbol -> unit
-
   (** Creates a new parameter set *)
   val mk_params : context -> params
 
@@ -583,16 +573,7 @@ sig
 
   (** Indicates whether the term is an implication *)
   val is_implies : Expr.expr -> bool
-
-  (** Indicates whether the term is a label (used by the Boogie Verification condition generator).
-     The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula. *)
-  val is_label : Expr.expr -> bool
-  
-  (** Indicates whether the term is a label literal (used by the Boogie Verification condition generator).                     
-     A label literal has a set of string parameters. It takes no arguments.
-     let is_label_lit ( x : expr ) = (FuncDecl.get_decl_kind (get_func_decl x) == OP_LABEL_LIT) *)
-  val is_label_lit : Expr.expr -> bool
-  
+ 
   (** Indicates whether the term is a binary equivalence modulo namings. 
      This binary predicate is used in proof terms.
      It captures equisatisfiability and equivalence modulo renamings. *)
@@ -1261,29 +1242,29 @@ sig
        The semantics of this function follows the SMT-LIB standard for the function to_int.
        The argument must be of real sort. *)
     val mk_real2int : context -> Expr.expr -> Expr.expr
-  end
-
-  (** Algebraic Numbers *)
-  module AlgebraicNumber :
-  sig
-    (** Return a upper bound for a given real algebraic number. 
-	The interval isolating the number is smaller than 1/10^precision.
-	{!is_algebraic_number}   
-	@return A numeral Expr of sort Real *)
-    val to_upper : Expr.expr -> int -> Expr.expr
-
-    (** Return a lower bound for the given real algebraic number. 
-	The interval isolating the number is smaller than 1/10^precision.
-	{!is_algebraic_number}
-	@return A numeral Expr of sort Real *)
-    val to_lower : Expr.expr -> int -> Expr.expr
-
-    (** Returns a string representation in decimal notation. 
-	The result has at most as many decimal places as the int argument provided.*)
-    val to_decimal_string : Expr.expr -> int -> string
-
-    (** Returns a string representation of the numeral. *)
-    val to_string : Expr.expr -> string
+      
+    (** Algebraic Numbers *)
+    module AlgebraicNumber :
+    sig
+      (** Return a upper bound for a given real algebraic number. 
+	  The interval isolating the number is smaller than 1/10^precision.
+	  {!is_algebraic_number}   
+	  @return A numeral Expr of sort Real *)
+      val to_upper : Expr.expr -> int -> Expr.expr
+	
+      (** Return a lower bound for the given real algebraic number. 
+	  The interval isolating the number is smaller than 1/10^precision.
+	  {!is_algebraic_number}
+	  @return A numeral Expr of sort Real *)
+      val to_lower : Expr.expr -> int -> Expr.expr
+	
+      (** Returns a string representation in decimal notation. 
+	  The result has at most as many decimal places as the int argument provided.*)
+      val to_decimal_string : Expr.expr -> int -> string
+	
+      (** Returns a string representation of the numeral. *)
+      val to_string : Expr.expr -> string
+    end
   end
 
   (** Indicates whether the term is of integer sort. *)
@@ -2389,19 +2370,16 @@ sig
   (** All symbols that have an interpretation in the model. *)
   val get_decls : model -> FuncDecl.func_decl list
 
-  (** A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. *)
-  exception ModelEvaluationFailedException of string
-
   (** Evaluates an expression in the current model.
       
       This function may fail if the argument contains quantifiers, 
       is partial (MODEL_PARTIAL enabled), or if it is not well-sorted.
       In this case a <c>ModelEvaluationFailedException</c> is thrown.
   *)
-  val eval : model -> Expr.expr -> bool -> Expr.expr
+  val eval : model -> Expr.expr -> bool -> Expr.expr option
 
   (** Alias for <c>eval</c>. *)
-  val evaluate : model -> Expr.expr -> bool -> Expr.expr
+  val evaluate : model -> Expr.expr -> bool -> Expr.expr option
 
   (** The number of uninterpreted sorts that the model has an interpretation for. *)
   val get_num_sorts : model -> int
@@ -2438,7 +2416,7 @@ sig
   type probe 
 
   (** Execute the probe over the goal. 
-     <returns>A probe always produce a double value.
+     <returns>A probe always produce a float value.
      "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns> *)
   val apply : probe -> Goal.goal -> float
 
@@ -2637,7 +2615,7 @@ sig
       (** True if the entry is uint-valued. *)
       val is_int : statistics_entry -> bool
 	
-      (** True if the entry is double-valued. *)
+      (** True if the entry is float-valued. *)
       val is_float : statistics_entry -> bool
 	
       (** The string representation of the the entry's value. *)
@@ -2954,10 +2932,11 @@ val get_global_param : string -> string option
     {!set_global_param}
 *)
 
-val global_param_reset_all : unit
-
-  (** Enable/disable printing of warning messages to the console.
-
-     Note that this function is static and effects the behaviour of 
-     all contexts globally. *)
-  val toggle_warning_messages : bool -> unit
+val global_param_reset_all : unit -> unit
+  
+(** Enable/disable printing of warning messages to the console.
+    
+    Note that this function is static and effects the behaviour of 
+    all contexts globally. *)
+val toggle_warning_messages : bool -> unit
+