diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f49b80b15..24157d428 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1823,7 +1823,7 @@ ast * ast_manager::register_node_core(ast * n) {
         SASSERT(m_ast_table.contains(n));
     }
 
-    n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
+    n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 286f2864a..3a29384dd 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -223,10 +223,12 @@ void goal::process_not_or(bool save_first, app * f, proof * pr, expr_dependency
 }
 
 void goal::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    expr* g = nullptr;
+    proof_ref _pr(pr, m());
     if (m().is_and(f))
         process_and(save_first, to_app(f), pr, d, out_f, out_pr);
-    else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))
-        process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr);
+    else if (m().is_not(f, g) && m().is_or(g))
+        process_not_or(save_first, to_app(g), pr, d, out_f, out_pr);
     else if (save_first) {
         out_f  = f;
         out_pr = pr;