Skip to content

Commit b52e0c4

Browse files
committed
[TEST] Lift rlimit for Z3 index bound proof
1 parent fffd7cb commit b52e0c4

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

tests/python/arith/test_arith_z3.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -271,6 +271,7 @@ def test_z3_flattened_index_bound():
271271
expr = tirx.all(0 <= i * n + j, i * n + j < m * n)
272272
with analyzer.constraint_scope(tirx.all(0 <= i, i < m, 0 <= j, j < n, m > 0, n > 0)):
273273
assert not analyzer.can_prove(expr)
274+
analyzer.set_z3_rlimit(0)
274275
assert analyzer.can_prove(expr, SB)
275276

276277

0 commit comments

Comments
 (0)