Avoid push timing out - Githubissues

HarvardPL / formulog

Datalog with support for SMT queries and first-order functional programming

https://harvardpl.github.io/formulog/

Apache License 2.0

155 stars 10 forks source link

Avoid push timing out #36

Closed aaronbembenek closed 1 year ago

aaronbembenek commented 1 year ago

The SMT-LIB command push is subject to the same timeout as check-sat; however, if it times out, it leaves the solver in an unusable state. This PR resets the timeout to the max value before pushes. See https://github.com/Z3Prover/z3/issues/4713