diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 6e5474a64..e88db7d27 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -744,10 +744,9 @@ namespace polysat { return false; entry const* e0 = e; - do { entry const* n = e->next(); - while (n != first) { + while (n != e0) { entry const* n1 = n->next(); if (n1 == e) break;