Skip to content

Support overriding of global solving timeout per request#1044

Merged
JonathanSalwan merged 2 commits intoJonathanSalwan:dev-v0.9from
SweetVishnya:solving-timeout-override
Sep 8, 2021
Merged

Support overriding of global solving timeout per request#1044
JonathanSalwan merged 2 commits intoJonathanSalwan:dev-v0.9from
SweetVishnya:solving-timeout-override

Conversation

@SweetVishnya
Copy link
Contributor

The motivation of this PR is following. We would like to solve queries in parallel. And sometimes we need to change solving timeout for specific queries (e.g, to detect symbolic address bounds with a small timeout). Global timeout does not allow to have different timeout for parallel queries.

@JonathanSalwan
Copy link
Owner

JonathanSalwan commented Sep 8, 2021

Thanks for this MR. Looks good to me. Just one thing: can you add a comment to the timeout attribute of the Z3Solver class explaining what you said about global timeout and that some queries may need personal timeout.

      /*! \brief Solver engine using z3. */
      class Z3Solver : public SolverInterface {
        private:
          //! The SMT solver timeout. By default, unlimited.
          triton::uint32 timeout;

Cheers!

@SweetVishnya
Copy link
Contributor Author

Added docs.

@JonathanSalwan JonathanSalwan merged commit e05532a into JonathanSalwan:dev-v0.9 Sep 8, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants