From 583c40de1f84a19621bc93660d98b9b4bf27ba3f Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 3 Apr 2024 16:42:17 +0200 Subject: [PATCH] check --- src/sat/smt/polysat/viable.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 2895c46d1..c71e827d1 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -923,7 +923,8 @@ namespace polysat { SASSERT(!get_covered_interval(after).contains(before.value)); rational hole_len = r_interval::len(before.value, get_covered_interval(after).lo(), rational::power_of_two(m_num_bits)); - SASSERT(hole_len < rational::power_of_two(hole_bits)); // otherwise we missed a conflict at lower bit-width + // verbose_stream() << " hole_len " << hole_len << " should be < " << rational::power_of_two(hole_bits) << "\n"; + VERIFY(hole_len < rational::power_of_two(hole_bits)); // otherwise we missed a conflict at lower bit-width // no constraint needed for constant bounds if (t1.is_val() && t2.is_val())