mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #4508

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-07 16:28:53 -07:00
parent d2a12f6db5
commit 5f9973d8c4
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/ba_solver.cpp
View file

@ -330,7 +330,7 @@ namespace sat {
m_stats.m_num_conflicts++; m_stats.m_num_conflicts++;
TRACE("ba", display(tout, c, true); ); TRACE("ba", display(tout, c, true); );
if (!validate_conflict(c)) { if (!validate_conflict(c)) {
display(std::cout, c, true); IF_VERBOSE(0, display(verbose_stream(), c, true));
UNREACHABLE(); UNREACHABLE();
} }
SASSERT(validate_conflict(c)); SASSERT(validate_conflict(c));
@ -2941,6 +2941,8 @@ namespace sat {
void ba_solver::pre_simplify() { void ba_solver::pre_simplify() {
VERIFY(s().at_base_lvl()); VERIFY(s().at_base_lvl());
if (s().inconsistent())
return;
m_constraint_removed = false; m_constraint_removed = false;
xor_finder xf(s()); xor_finder xf(s());
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_constraints[i]); for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_constraints[i]);
@ -2983,6 +2985,8 @@ namespace sat {
void ba_solver::simplify() { void ba_solver::simplify() {
if (!s().at_base_lvl()) s().pop_to_base_level(); if (!s().at_base_lvl()) s().pop_to_base_level();
if (s().inconsistent())
return;
unsigned trail_sz, count = 0; unsigned trail_sz, count = 0;
do { do {
trail_sz = s().init_trail_size(); trail_sz = s().init_trail_size();