mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

move std::function initializer to beginning of class

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-16 17:02:15 -08:00
parent f6f594e21d
commit e16acd0965
2 changed files with 4 additions and 2 deletions

4
src/sat/smt/euf_solver.h
View file

@ -79,7 +79,8 @@ namespace euf {
return reinterpret_cast<size_t>(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<scope> m_scopes;
scoped_ptr_vector<th_solver> m_solvers;
ptr_vector<th_solver> m_id2solver;
std::function<::solver*(void)> m_mk_solver;
constraint* m_conflict{ nullptr };
constraint* m_eq{ nullptr };

2
src/smt/theory_seq.cpp
View file

@ -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)));