diff --git a/src/ast/ast.h b/src/ast/ast.h
index 408ca4063..34ea96653 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2474,15 +2474,15 @@ class justified_expr {
     ast_manager& m;
     expr*        m_fml;
     proof*       m_proof;
- public:
- justified_expr(ast_manager& m, expr* fml, proof* p):
-    m(m),
-    m_fml(fml),
-    m_proof(p) {
+public:
+    justified_expr(ast_manager& m, expr* fml, proof* p):
+        m(m),
+        m_fml(fml),
+        m_proof(p) {
         m.inc_ref(fml);
         m.inc_ref(p);
     }
-
+    
     justified_expr& operator=(justified_expr& other) {
         SASSERT(&m == &other.m);
         if (this != &other) {
diff --git a/src/smt/asserted_formulas_new.cpp b/src/smt/asserted_formulas_new.cpp
index 14c8615a2..39c432b61 100644
--- a/src/smt/asserted_formulas_new.cpp
+++ b/src/smt/asserted_formulas_new.cpp
@@ -467,7 +467,8 @@ unsigned asserted_formulas_new::propagate_values(unsigned i) {
         proof * pr  = m_formulas[i].get_proof();
         new_pr = m.mk_modus_ponens(pr, new_pr);                         
     }
-    m_formulas[i] = justified_expr(m, new_n, new_pr);
+    justified_expr j(m, new_n, new_pr);
+    m_formulas[i] = j;
     update_substitution(new_n, new_pr);
     return n != new_n ? 1 : 0;
 }