diff --git a/lib/goal.cpp b/lib/goal.cpp
index 0146ac252..71f3a097c 100644
--- a/lib/goal.cpp
+++ b/lib/goal.cpp
@@ -284,6 +284,30 @@ void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) cons
     out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
 }
 
+void goal::display_with_dependencies(std::ostream & out) const {
+    ptr_vector<expr> deps;
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  |-";
+        deps.reset();
+        m().linearize(dep(i), deps);
+        ptr_vector<expr>::iterator it  = deps.begin();
+        ptr_vector<expr>::iterator end = deps.end();
+        for (; it != end; ++it) {
+            expr * d = *it;
+            if (is_uninterp_const(d)) {
+                out << " " << mk_ismt2_pp(d, m());
+            }
+            else {
+                out << " #" << d->get_id();
+            }
+        }
+        out << "\n  " << mk_ismt2_pp(form(i), m(), 2);
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
 void goal::display(cmd_context & ctx) const {
     display(ctx, ctx.regular_stream());
 }
diff --git a/lib/goal.h b/lib/goal.h
index 9beb9421e..61c7e2081 100644
--- a/lib/goal.h
+++ b/lib/goal.h
@@ -180,6 +180,7 @@ public:
     void display_dimacs(std::ostream & out) const;
     void display_with_dependencies(cmd_context & ctx, std::ostream & out) const;
     void display_with_dependencies(cmd_context & ctx) const;
+    void display_with_dependencies(std::ostream & out) const;
 
     bool sat_preserved() const { 
         return prec() == PRECISE || prec() == UNDER; 
diff --git a/lib/simplify_tactic.cpp b/lib/simplify_tactic.cpp
index 2a912822b..a7ce0b39f 100644
--- a/lib/simplify_tactic.cpp
+++ b/lib/simplify_tactic.cpp
@@ -67,6 +67,7 @@ struct simplify_tactic::imp {
         TRACE("after_simplifier_bug", g.display(tout););
         g.elim_redundancies();
         TRACE("after_simplifier", g.display(tout););
+        TRACE("after_simplifier_detail", g.display_with_dependencies(tout););
         SASSERT(g.is_well_sorted());
     }