diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 970a96c72..1a2def0c8 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2587,9 +2587,9 @@ namespace z3 {
 
         friend std::ostream & operator<<(std::ostream & out, model const & m);
 
-        std::string to_string() const { return std::string(Z3_model_to_string(ctx(), m_model)); }
+        std::string to_string() const { return m_model ? std::string(Z3_model_to_string(ctx(), m_model)) : "null"; }
     };
-    inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }
+    inline std::ostream & operator<<(std::ostream & out, model const & m) { return out << m.to_string(); }
 
     class stats : public object {
         Z3_stats m_stats;
@@ -3983,6 +3983,7 @@ namespace z3 {
             scoped_cb _cb(p, cb);
             expr value(p->ctx(), _value);
             expr var(p->ctx(), _var);
+            std::cout << "Fixed " << cb << "\n";
             p->m_fixed_eh(var, value);
         }
 
@@ -4150,6 +4151,7 @@ namespace z3 {
             assert(cb);
             expr conseq = ctx().bool_val(false);
             array<Z3_ast> _fixed(fixed);
+            std::cout << "conflict " << cb << " " << fixed << "\n";
             Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
         }
 
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 751386ef3..3f5310ce5 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -100,7 +100,7 @@ theory * theory_user_propagator::mk_fresh(context * new_ctx) {
         ctx = m_fresh_eh(m_user_context, new_ctx->get_manager(), th->m_api_context);
     }
     catch (...) {
-      throw default_exception("Exception thrown in \"fresh\"-callback");
+        throw default_exception("Exception thrown in \"fresh\"-callback");
     }
     th->add(ctx, m_push_eh, m_pop_eh, m_fresh_eh);
     if ((bool)m_fixed_eh) th->register_fixed(m_fixed_eh);
@@ -140,7 +140,7 @@ void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned nu
          m_fixed_eh(m_user_context, this, var2expr(v), value);
      }
      catch (...) {
-       throw default_exception("Exception thrown in \"fixed\"-callback");
+        throw default_exception("Exception thrown in \"fixed\"-callback");
      }
 }
 
@@ -252,7 +252,7 @@ bool theory_user_propagator::internalize_term(app* term)  {
         m_created_eh(m_user_context, this, term);
     }
     catch (...) {
-      throw default_exception("Exception thrown in \"created\"-callback");
+        throw default_exception("Exception thrown in \"created\"-callback");
     }
 
     return true;