diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h
index ae02e371e..bbd1c0e8e 100644
--- a/src/ast/expr_substitution.h
+++ b/src/ast/expr_substitution.h
@@ -51,7 +51,7 @@ public:
     void reset();
     void cleanup();
 
-    obj_map<expr, expr*> const sub() const { return m_subst; }
+    obj_map<expr, expr*> const & sub() const { return m_subst; }
 
     std::ostream& display(std::ostream& out);
 };
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index 22af58d59..7a48f8809 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -147,6 +147,7 @@ namespace sat {
             if (m_solver.value(r) == l_true)
                 lits.push_back(r);
         out << "roots: " << lits << "\n";
+        m_solver.display(out);
 
         return out;
     }