mirror of
https://github.com/Z3Prover/z3
synced 2025-07-03 03:15:41 +00:00
check
This commit is contained in:
parent
4a51139bc8
commit
583c40de1f
1 changed files with 2 additions and 1 deletions
|
@ -923,7 +923,8 @@ namespace polysat {
|
||||||
SASSERT(!get_covered_interval(after).contains(before.value));
|
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));
|
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
|
// no constraint needed for constant bounds
|
||||||
if (t1.is_val() && t2.is_val())
|
if (t1.is_val() && t2.is_val())
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue