mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2024-03-21 12:03:52 +01:00
parent acd05686e4
commit 342db52558
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/viable.cpp
View file

@ -665,10 +665,12 @@ namespace polysat {
switch (m_projection()) { switch (m_projection()) {
case l_true: case l_true:
// propagated interval onto subslice // propagated interval onto subslice
result.reset();
m_projection.explain(result); m_projection.explain(result);
break; break;
case l_false: case l_false:
// conflict (projected interval is full) // conflict (projected interval is full)
result.reset();
m_projection.explain(result); m_projection.explain(result);
break; break;
case l_undef: case l_undef: