diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 7a7deb573..dedaa53be 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -665,10 +665,12 @@ namespace polysat { switch (m_projection()) { case l_true: // propagated interval onto subslice + result.reset(); m_projection.explain(result); break; case l_false: // conflict (projected interval is full) + result.reset(); m_projection.explain(result); break; case l_undef: