diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 8dd7f6943..97413ae54 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -3882,7 +3882,7 @@ namespace z3 {
 
 
     public:
-        user_propagator_base(context* c) : s(nullptr), c(c) {}
+        user_propagator_base(Z3_context c) : s(nullptr), c(c) {}
         
         user_propagator_base(solver* s): s(s), c(nullptr) {
               Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index f6f61cd83..86fc5fcce 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -275,7 +275,6 @@ namespace array {
      * e1 = e2 or select(e1, diff(e1,e2)) != select(e2, diff(e1, e2))
      */
     bool solver::assert_extensionality(expr* e1, expr* e2) {
-        TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n";);
         ++m_stats.m_num_extensionality_axiom;
         func_decl_ref_vector const& funcs = sort2diff(e1->get_sort());
         expr_ref_vector args1(m), args2(m);
@@ -290,6 +289,7 @@ namespace array {
         expr_ref sel2(a.mk_select(args2), m);
         literal lit1 = eq_internalize(e1, e2);
         literal lit2 = eq_internalize(sel1, sel2);
+        TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n" << lit1 << " " << ~lit2 << "\n";);
         return add_clause(lit1, ~lit2);
     }
 
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index d2fa19eee..178225179 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -277,9 +277,15 @@ namespace euf {
             if (!tt && !mdl.is_true(e))
                 continue;
             IF_VERBOSE(0, 
-                       verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
-                       for (auto* arg : euf::enode_args(n))
-                           verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n";);
+                verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
+                for (auto* arg : euf::enode_args(n)) {
+                    expr_ref val = mdl(arg->get_expr());
+                    expr_ref sval(m);
+                    th_rewriter rw(m);
+                    rw(val, sval);
+                    verbose_stream() << bpp(arg) << "\n" << sval << "\n";
+
+                });
             CTRACE("euf", first, 
                    tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
                    s().display(tout);