Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

rlimit fails to stop z3 #7247

Closed hmijail closed 3 weeks ago

hmijail commented 1 month ago

I have a generated file that keeps z3 working "forever" even if I give it a rlimit.

$ z3-4.13.0/bin/z3 1717648676-Impl__name.__default.block__0__0x0128_split20.smt rlimit=6900000
...

Interestingly, making the rlimit slightly lower causes z3 to finish in ~1 second.

$ z3-4.13.0/bin/z3 1717648676-Impl__name.__default.block__0__0x0128_split20.smt rlimit=6700000
unknown
(:reason-unknown "canceled")
(:rlimit 6722629)

This is on macOS 14.5 (ARM), z3 4.13.0. Also reproducible with previous z3 versions (4.12.6... 4.12.1).

1717648676-Implname.default.block00x0128_split20.smt.zip

NikolajBjorner commented 3 weeks ago

35c1cacf44951787e1427a4b76941f961aff4584