mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 00:53:25 +00:00
Code Activity

fix #3631

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 21:00:52 -07:00
parent ddc77b1100
commit 1d6fb6352f
1 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/ba_solver.cpp
View file

@ -2076,12 +2076,20 @@ namespace sat {
else else
polarity = polarity ^ sign; polarity = polarity ^ sign;
} }
if (lits.empty()) { if (polarity && !lits.empty()) {
throw default_exception("empty xor is TBD");
}
if (polarity) {
lits[0].neg(); lits[0].neg();
} }
switch (lits.size()) {
case 0:
if (polarity)
s().set_conflict(justification(0));
return nullptr;
case 1:
s().assign_scoped(lits[0]);
return nullptr;
default:
break;
}
void * mem = m_allocator.allocate(xr::get_obj_size(lits.size())); void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
xr* x = new (mem) xr(next_id(), lits); xr* x = new (mem) xr(next_id(), lits);
x->set_learned(learned); x->set_learned(learned);