diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index f0f455f6c..21a02909e 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -46,6 +46,7 @@ namespace euf {
                 value = r->get_expr();
             else
                 value = factory.get_fresh_value(srt);
+            (void)s;
             TRACE("model", tout << s.bpp(r) << " := " << value << "\n";);
             values.set(id, value);
             expr_ref_vector* vals = nullptr;
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index d53773f0d..9203c35bd 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1145,7 +1145,7 @@ bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const&
         m.inc_ref(rhs);
         m.inc_ref(ls[0]);
         m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0]));
-        ctx.push_trail(remove_obj_pair_map(m, m_nth_eq2_cache, rhs, ls[0]));
+        get_trail_stack().push(remove_obj_pair_map(m, m_nth_eq2_cache, rhs, ls[0]));
         ls1.push_back(s);        
         if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx)); 
         rs1.push_back(m_util.str.mk_unit(rhs));