Skip to content

Commit fffd7cb

Browse files
committed
[TEST] Lift rlimit for Z3 monotonicity proof
1 parent 6be6a9e commit fffd7cb

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
@@ -231,6 +231,7 @@ def test_z3_floor_division_monotonicity():
231231
c = tirx.Var("c", "int32")
232232
expr = implies(tirx.all(a <= b, c > 0), tirx.floordiv(a, c) <= tirx.floordiv(b, c))
233233
assert not analyzer.can_prove(expr)
234+
analyzer.set_z3_rlimit(0)
234235
assert analyzer.can_prove(expr, SB)
235236

236237

0 commit comments

Comments
 (0)