mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
build fix
This commit is contained in:
parent
a152bb1e80
commit
55cb12e233
|
@ -315,7 +315,7 @@ public:
|
|||
m_solver.set_phase(lit);
|
||||
}
|
||||
void move_to_front(expr* e) override {
|
||||
bool is_not = m.is_not(e, e);
|
||||
m.is_not(e, e);
|
||||
sat::bool_var b = m_map.to_bool_var(e);
|
||||
if (b != sat::null_bool_var)
|
||||
m_solver.move_to_front(b);
|
||||
|
|
|
@ -31,7 +31,7 @@ namespace bv {
|
|||
public:
|
||||
bit_trail(solver& s, var_pos vp) : s(s), vp(vp), lit(s.m_bits[vp.first][vp.second]) {}
|
||||
|
||||
virtual void undo(euf::solver& euf) {
|
||||
void undo() override {
|
||||
s.m_bits[vp.first][vp.second] = lit;
|
||||
}
|
||||
};
|
||||
|
@ -43,7 +43,7 @@ namespace bv {
|
|||
public:
|
||||
bit_occs_trail(solver& s, atom& a): a(a), m_occs(a.m_occs) {}
|
||||
|
||||
virtual void undo() {
|
||||
void undo() override {
|
||||
a.m_occs = m_occs;
|
||||
}
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue