diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml
index f7a4cbc00..c9ed1d948 100644
--- a/examples/ml/ml_example.ml
+++ b/examples/ml/ml_example.ml
@@ -29,11 +29,11 @@ let  model_converter_test ( ctx : context ) =
   let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in
   let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in
   let g4 = (mk_goal ctx true false false ) in
-  (Goal.assert_ g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
-  (Goal.assert_ g4 [ (mk_eq ctx 
+  (Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
+  (Goal.add g4 [ (mk_eq ctx 
 			 yr
 			 (Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1)  ])) ]) ;
-  (Goal.assert_ g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ;
+  (Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ;
   (
     let  ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
     if ((get_num_subgoals ar) == 1 && 
@@ -53,7 +53,7 @@ let  model_converter_test ( ctx : context ) =
       Printf.printf "Test passed.\n"
     ;
     let solver = (mk_solver ctx None) in
-    let f e = (Solver.assert_ solver [ e ]) in
+    let f e = (Solver.add solver [ e ]) in
     ignore (List.map f (get_formulas (get_subgoal ar 0))) ;
     let q = (check solver []) in
     if q != SATISFIABLE then 
@@ -88,12 +88,12 @@ let basic_tests ( ctx : context ) =
   let trivial_eq = (mk_eq ctx fapp fapp) in
   let nontrivial_eq = (mk_eq ctx fapp fapp2) in
   let g = (mk_goal ctx true false false) in
-  (Goal.assert_ g [ trivial_eq ]) ;
-  (Goal.assert_ g [ nontrivial_eq ]) ;
+  (Goal.add g [ trivial_eq ]) ;
+  (Goal.add g [ nontrivial_eq ]) ;
   Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ;
   (
     let solver = (mk_solver ctx None) in
-    (List.iter (fun a -> (Solver.assert_ solver [ a ])) (get_formulas g)) ;
+    (List.iter (fun a -> (Solver.add solver [ a ])) (get_formulas g)) ;
     if (check solver []) != SATISFIABLE then
       raise (TestFailedException "")
     else
@@ -116,7 +116,7 @@ let basic_tests ( ctx : context ) =
     else
       Printf.printf "Test passed.\n"
   );
-  (Goal.assert_ g [ (mk_eq ctx 
+  (Goal.add g [ (mk_eq ctx 
 			(mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32))
 			(mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] )
   ;
@@ -139,7 +139,7 @@ let basic_tests ( ctx : context ) =
   );
   (
     let g2 = (mk_goal ctx true true false) in
-    (Goal.assert_ g2 [ (Boolean.mk_false ctx) ]) ;
+    (Goal.add g2 [ (Boolean.mk_false ctx) ]) ;
     let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
     if ((get_num_subgoals ar) == 1 && 
 	   (not (is_decided_unsat (get_subgoal ar 0)))) then
@@ -151,10 +151,10 @@ let basic_tests ( ctx : context ) =
     let g3 = (mk_goal ctx true true false) in
     let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Integer.mk_sort ctx)) in
     let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Integer.mk_sort ctx)) in
-    (Goal.assert_ g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ;
-    (Goal.assert_ g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ;
+    (Goal.add g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ;
+    (Goal.add g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ;
     let constr = (mk_eq ctx xc yc) in
-    (Goal.assert_ g3 [ constr ] ) ;
+    (Goal.add g3 [ constr ] ) ;
     let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in
     if ((get_num_subgoals ar) == 1 && 
 	   (not (is_decided_unsat (get_subgoal ar 0)))) then
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index e62732924..8eb5427bb 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1850,7 +1850,7 @@ struct
   let is_garbage ( x : goal ) = 
     (get_precision x) == GOAL_UNDER_OVER
       
-  let assert_ ( x : goal ) ( constraints : expr list ) =
+  let add ( x : goal ) ( constraints : expr list ) =
     let f e = Z3native.goal_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e) in
     ignore (List.map f constraints) ;
     ()
@@ -2370,11 +2370,11 @@ struct
 
   let reset ( x : solver ) = Z3native.solver_reset (z3obj_gnc x) (z3obj_gno x)
 
-  let assert_ ( x : solver ) ( constraints : expr list ) =
+  let add ( x : solver ) ( constraints : expr list ) =
     let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) in
     ignore (List.map f constraints)
 
-  let assert_and_track_a ( x : solver ) ( cs : expr list ) ( ps : expr list ) =
+  let assert_and_track_l ( x : solver ) ( cs : expr list ) ( ps : expr list ) =
     if ((List.length cs) != (List.length ps)) then
       raise (Z3native.Exception "Argument size mismatch")
     else
@@ -2473,7 +2473,7 @@ struct
   let get_param_descrs ( x : fixedpoint ) =
     Params.ParamDescrs.param_descrs_of_ptr (z3obj_gc x) (Z3native.fixedpoint_get_param_descrs (z3obj_gnc x) (z3obj_gno x))
       
-  let assert_ ( x : fixedpoint ) ( constraints : expr list ) =
+  let add ( x : fixedpoint ) ( constraints : expr list ) =
     let f e = (Z3native.fixedpoint_assert (z3obj_gnc x) (z3obj_gno x) (Expr.gno e)) in
     ignore (List.map f constraints) ;
     ()
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index d7e179cd4..cde99a90d 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -2221,7 +2221,7 @@ sig
   val is_garbage : goal -> bool
 
  (** Adds the constraints to the given goal. *)
-  val assert_ : goal -> Expr.expr list -> unit
+  val add : goal -> Expr.expr list -> unit
  
   (** Indicates whether the goal contains `false'. *)
   val is_inconsistent : goal -> bool
@@ -2648,7 +2648,7 @@ sig
   val reset : solver -> unit
 
   (** Assert a constraint (or multiple) into the solver. *)        
-  val assert_ : solver -> Expr.expr list -> unit
+  val add : solver -> Expr.expr list -> unit
 
   (** * Assert multiple constraints (cs) into the solver, and track them (in the
      * unsat) core
@@ -2661,7 +2661,7 @@ sig
      * of the Boolean variables provided using {!assert_and_track}
      * and the Boolean literals
      * provided using {!check} with assumptions. *)
-  val assert_and_track_a : solver -> Expr.expr list -> Expr.expr list -> unit
+  val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit
 
   (** * Assert a constraint (c) into the solver, and track it (in the unsat) core
      * using the Boolean constant p.
@@ -2752,7 +2752,7 @@ sig
   val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs
 
   (** Assert a constraints into the fixedpoint solver. *)        
-  val assert_ : fixedpoint -> Expr.expr list -> unit
+  val add : fixedpoint -> Expr.expr list -> unit
 
   (** Register predicate as recursive relation. *)       
   val register_relation : fixedpoint -> FuncDecl.func_decl -> unit