diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index e88db7d27..96b468d10 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -755,6 +755,11 @@ namespace polysat { break; n = n1; } + if (e == n) { + SASSERT_EQ(e, e0); + // VERIFY(false); + return false; + } if (e == e0) { out_lo = n->interval.lo_val();