From dd1e0fc561196bbe097e45fe5876a00ca2d152c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Nov 2021 08:49:33 -0700 Subject: [PATCH] #5643 --- src/sat/smt/euf_model.cpp | 1 + src/smt/seq_eq_solver.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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));