From e16acd0965bcb679e54c451eba61a4a8ed474a03 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Nov 2020 17:02:15 -0800 Subject: [PATCH] move std::function initializer to beginning of class Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.h | 4 ++-- src/smt/theory_seq.cpp | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index b9dba36f7..d134673ee 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -79,7 +79,8 @@ namespace euf { return reinterpret_cast(UNTAG(size_t*, p)); } - ast_manager& m; + std::function<::solver*(void)> m_mk_solver; + ast_manager& m; sat::sat_internalizer& si; smt_params m_config; euf::egraph m_egraph; @@ -102,7 +103,6 @@ namespace euf { svector m_scopes; scoped_ptr_vector m_solvers; ptr_vector m_id2solver; - std::function<::solver*(void)> m_mk_solver; constraint* m_conflict{ nullptr }; constraint* m_eq{ nullptr }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3d2a6231d..863e8f3f9 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -501,6 +501,8 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) { TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";); literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false); literal b = mk_seq_eq(seq, e); + if (ctx.get_assignment(a) == l_false || ctx.get_assignment(b) == l_true) + return false; add_axiom(~a, b); if (!ctx.at_base_level()) { m_trail_stack.push(push_replay(alloc(replay_fixed_length, m, len_e)));