tlopex opened a new pull request, #20097: URL: https://github.com/apache/tvm/pull/20097
This PR improves the reliability and determinism of the Z3 arithmetic prover by introducing scoped Z3 contexts, safely preserving context ownership when cloning analyzers, and replacing unordered-map-owned Z3 expressions with a deterministic memo pool and reusable slots. It prevents Z3 AST allocation history and hash iteration order from affecting `CanProve` results under resource limits, while adding regression coverage for context lifetime, memo cleanup, slot reuse, and analyzer cloning. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected] --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
