mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

fix #3142

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-04 14:27:32 -08:00
parent 29f3f6a7aa
commit 76d91f7d2b
3 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2602,13 +2602,14 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
}
br_status st;
if (m_bit2bool) {
if (m_bit2bool && false) {
st = mk_bit2bool(lhs, rhs, result);
if (st != BR_FAILED)
return st;
}
if (m_trailing) {
st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
m_rm_trailing.reset_cache(1 << 12);
if (st != BR_FAILED) {

7
src/sat/sat_solver.cpp
View file

@ -1317,6 +1317,13 @@ namespace sat {
lbool solver::do_unit_walk() {
unit_walk srch(*this);
lbool r = srch();
if (r == l_true) {
m_model.reset();
for (bool_var v = 0; v < num_vars(); ++v) {
m_model.push_back(m_assignment[literal(v,false).index()]);
}
m_model_is_current = true;
}
return r;
}

1
src/sat/sat_unit_walk.h
View file

@ -71,6 +71,7 @@ namespace sat {
bool m_inconsistent;
literal_vector m_decisions;
unsigned m_conflict_offset;
svector<lbool> m_model;
bool should_restart();
void do_pop();