diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 10af489cf..5173a0afd 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -1506,6 +1506,12 @@ namespace seq {
                                                                   : "UNKNOWN")
                                   << "\n";);
                 if (r == search_result::sat) {
+                    IF_VERBOSE(
+                        1, 
+                        verbose_stream() << "side constraints: \n";
+                        for (auto const &c : m_cur_path.back()->side_constraints()) {
+                            verbose_stream() << "  side constraint: " << c.fml << "\n";
+                        });
                     ++m_stats.m_num_sat;
                     return r;
                 }
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index e03db5a44..a703d6135 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -744,7 +744,6 @@ namespace seq {
         ast_manager&                  m;
         seq_util&                     m_seq;
         euf::sgraph&                  m_sg;
-        // region                        m_region;
         ptr_vector<nielsen_node>      m_nodes;
         ptr_vector<nielsen_edge>      m_edges;
         nielsen_node*                 m_root = nullptr;