diff --git a/scripts/update_api.py b/scripts/update_api.py
index bb5935a1e..86f6ceee8 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -57,7 +57,7 @@ log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }
 log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n')
 log_h.write('void _Z3_append_log(char const * msg);\n')
 ##
-exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg_ex(ctx, c)); }\n')
+exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
 ##
 core_py.write('# Automatically generated file\n')
 core_py.write('import sys, os\n')
@@ -404,7 +404,7 @@ def mk_py_wrappers():
         if len(params) > 0 and param_type(params[0]) == CONTEXT:
             core_py.write("  err = lib().Z3_get_error_code(a0)\n")
             core_py.write("  if err != Z3_OK:\n")
-            core_py.write("    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))\n")
+            core_py.write("    raise Z3Exception(lib().Z3_get_error_msg(a0, err))\n")
         if result == STRING:
             core_py.write("  return _to_pystr(r)\n")
         elif result != VOID:
@@ -477,7 +477,7 @@ def mk_dotnet_wrappers():
     dotnet.write("            LIB.Z3_set_error_handler(a0, a1);\n")
     dotnet.write("            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
     dotnet.write("            if (err != Z3_error_code.Z3_OK)\n")
-    dotnet.write("                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
+    dotnet.write("                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
     dotnet.write("        }\n\n")
     for name, result, params in _dotnet_decls:
         if result == STRING:
@@ -525,7 +525,7 @@ def mk_dotnet_wrappers():
                 if len(params) > 0 and param_type(params[0]) == CONTEXT:
                     dotnet.write("            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
                     dotnet.write("            if (err != Z3_error_code.Z3_OK)\n")
-                    dotnet.write("                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
+                    dotnet.write("                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
         if result == STRING:
             dotnet.write("            return Marshal.PtrToStringAnsi(r);\n")
         elif result != VOID:
@@ -1276,7 +1276,7 @@ def mk_ml():
         if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT:
             ml_native.write('    let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n')
             ml_native.write('      if err <> OK then\n')
-            ml_native.write('        raise (Exception (ML2C.n_get_error_msg_ex a0 (int_of_error_code err)))\n')
+            ml_native.write('        raise (Exception (ML2C.n_get_error_msg a0 (int_of_error_code err)))\n')
             ml_native.write('      else\n')
         if result == VOID and len(op) == 0:
             ml_native.write('        ()\n')
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 9c1701c44..c1f982997 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -33,7 +33,7 @@ void install_tactics(tactic_manager & ctx);
 namespace api {
 
     static void default_error_handler(Z3_context ctx, Z3_error_code c) {
-        printf("Error: %s\n", Z3_get_error_msg_ex(ctx, c));
+        printf("Error: %s\n", Z3_get_error_msg(ctx, c));
         exit(1);
     }
 
@@ -531,7 +531,7 @@ extern "C" {
         SET_ERROR_CODE(e);
     }
 
-    static char const * _get_error_msg_ex(Z3_context c, Z3_error_code err) {
+    static char const * _get_error_msg(Z3_context c, Z3_error_code err) {
         switch(err) {
         case Z3_OK:                return "ok";
         case Z3_SORT_ERROR:        return "type error";
@@ -551,9 +551,9 @@ extern "C" {
     }
 
 
-    Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
-        LOG_Z3_get_error_msg_ex(c, err);
-        return _get_error_msg_ex(c, err);
+    Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) {
+        LOG_Z3_get_error_msg(c, err);
+        return _get_error_msg(c, err);
     }
 
 
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 77848900e..6112a8cd2 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -391,7 +391,6 @@ extern "C" {
     }
 
 
-#if 0
     Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, 
                                               Z3_solver s,
                                               unsigned num_terms,
@@ -407,6 +406,5 @@ extern "C" {
         return static_cast<Z3_lbool>(result); 
         Z3_CATCH_RETURN(Z3_L_UNDEF);
     }
-#endif
 
 };
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 798ffe2cf..4492a4c0f 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5323,9 +5323,9 @@ BEGIN_MLAPI_EXCLUDE
     /**
        \brief Return a string describing the given error code.
 
-       def_API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
+       def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
     */
-    Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
+    Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
 END_MLAPI_EXCLUDE
 #ifdef ML4only
 #include <mlx_get_error_msg.idl>
@@ -7216,6 +7216,37 @@ END_MLAPI_EXCLUDE
     Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, 
                                                 unsigned num_assumptions, Z3_ast const assumptions[]);
 
+
+
+#ifdef CorML4
+    /**
+       \brief Retrieve congruence class representatives for terms.
+
+       The function can be used for relying on Z3 to identify equal terms under the current
+       set of assumptions. The array of terms and array of class identifiers should have
+       the same length. The class identifiers are numerals that are assigned to the same
+       value for their corresponding terms if the current context forces the terms to be
+       equal. You cannot deduce that terms corresponding to different numerals must be all different, 
+       (especially when using non-convex theories).
+       All implied equalities are returned by this call.
+       This means that two terms map to the same class identifier if and only if
+       the current context implies that they are equal.
+
+       A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in.
+       The function return Z3_L_FALSE if the current assertions are not satisfiable.
+
+    
+
+       def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
+    */
+    Z3_lbool Z3_API Z3_get_implied_equalities(
+        Z3_context c, 
+        Z3_solver  s, 
+        unsigned num_terms,
+        Z3_ast const terms[],
+        unsigned class_ids[]
+        );
+#endif
     /**
        \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions
 
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index d349da4ec..39e519863 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -738,6 +738,7 @@ namespace pdr {
     // model_node
 
     void model_node::set_closed() {
+        TRACE("pdr", tout << state() << "\n";);
         pt().close(state());
         m_closed = true; 
     }
@@ -1149,17 +1150,21 @@ namespace pdr {
             ast_manager& m = n->pt().get_manager();
             if (!n->get_model_ptr()) {
                 if (models.find(n->state(), md)) {
-                    TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
+                    TRACE("pdr", tout << n->state() << "\n";);
                     model_ref mr(md);
                     n->set_model(mr);
                     datalog::rule const* rule = rules.find(n->state());
                     n->set_rule(rule);
                 }
                 else {
+  		    TRACE("pdr", tout << "no model for " << n->state() << "\n";);
                     IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0);
-                               verbose_stream() << mk_pp(n->state(), m) << "\n";);
+                               verbose_stream() << n->state() << "\n";);
                 }
             }
+	    else {
+	         TRACE("pdr", tout << n->state() << "\n";);
+	    }
             todo.pop_back();
             todo.append(n->children().size(), n->children().c_ptr());
         }        
@@ -2027,11 +2032,11 @@ namespace pdr {
             switch (expand_state(n, cube, uses_level)) {
             case l_true:
                 if (n.level() == 0) {
-                    TRACE("pdr", tout << "reachable at level 0\n";);
+  		    TRACE("pdr", n.display(tout << "reachable at level 0\n", 0););
                     close_node(n);
                 }
                 else {
-                    TRACE("pdr", tout << "node: " << &n << "\n";); 
+ 	 	    TRACE("pdr", n.display(tout, 0);); 
                     create_children(n);
                 }
                 break;
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 7cba1e0c5..35b9067b2 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -240,7 +240,7 @@ namespace pdr {
         void check_pre_closed();
         void set_closed();     
         void set_open();
-        void set_pre_closed() { m_closed = true; }
+        void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; }
         void reset() { m_children.reset(); }
 
         void set_rule(datalog::rule const* r) { m_rule = r; }