mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

unused variable

Browse source
This commit is contained in:
Jakob Rath 2023-03-17 23:25:20 +01:00
parent 317fed1062
commit a10a7e31a6
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/solver.cpp
View file

@ -771,8 +771,6 @@ namespace polysat {
case trail_instr_t::assign_bool_i: { case trail_instr_t::assign_bool_i: {
sat::literal lit = m_search.back().lit(); sat::literal lit = m_search.back().lit();
LOG_V(20, "Undo assign_bool_i: " << lit_pp(*this, lit)); LOG_V(20, "Undo assign_bool_i: " << lit_pp(*this, lit));
unsigned active_level = m_bvars.level(lit);
clause* reason = m_bvars.reason(lit); clause* reason = m_bvars.reason(lit);
if (reason && reason->size() == 1) { if (reason && reason->size() == 1) {
SASSERT(m_bvars.is_bool_propagation(lit)); SASSERT(m_bvars.is_bool_propagation(lit));