Closed parno closed 3 years ago
We could also make the types long rather than int. I don't know if there are standardized limits for SMT solvers. But your solution is fine too.
Z3 describes both timeout
and rlimit
as unsigned int, with a default of 4294967295 for timeout
, so I think we're likely limited to 32 bits here. I created two possible patches for the issue.
This one is a minimal change that only directly affects the SetTimeout
and SetRlimit
methods:
https://github.com/parno/boogie/commit/d4728c6c280a6b12f5901fa76e1b25721e3106b6
This one systematically converts time limits into uint
, which seems like the "right" answer (since a negative time limit is perplexing), but it has a more pervasive effect, and I don't know if it risks breaking Boogie clients.
https://github.com/parno/boogie/commit/7a88665926ce775c5d45e6b350a4da42dba1638d
Any preferences?
The uint
solution looks fine to me.
When passed a large timeLimit or rlimit attribute, e.g., in this snippet:
these lines: https://github.com/boogie-org/boogie/blob/462b86feb73dfe7c23d5657380cb6837679c7728/Source/VCGeneration/Checker.cs#L205 https://github.com/boogie-org/boogie/blob/462b86feb73dfe7c23d5657380cb6837679c7728/Source/VCGeneration/Checker.cs#L210 multiply by 1000, causing an integer overflow. As a result, Boogie passes a negative value to Z3, which objects with
I would propose that we should detect when an overflow might happen and instead send the maximum
int
value, but I wanted to see if others had alternate proposals.