Solidity: Set timeout to single SMT query

[leonardoalt]

Whenever we ask the CVC4 or Z3 solvers to check input for satisfiability, we should somehow limit how much time they can spend looking for a solution. The same might apply when we ask for a model, if that is not already done as part of checking for satisfiability. At best, this is just a setting for Z3 and CVC4. In the worst case, we have to set up the solver in a separate thread and somehow kill the thread or do whatever is necessary. If more drastic measures are taken, it of course has to be fully portable.

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

__This issue now has a funding of 150.0 DAI (150.0 USD @ $1.0/DAI) attached to it.__

• If you would like to work on this issue you can 'start work' on the Gitcoin Issue Details page.
• Questions? Checkout Gitcoin Help or the Gitcoin Slack
• $4,479.63 more funded OSS Work available on the Gitcoin Issue Explorer

[gitcoinbot]

@pfilippi24 Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] auto removal (6 days)

[jmahhh]

Hi @leonardoalt I'm not super familiar with the workflow/implementation here but:

• for CVC4 one can use --tlimit-per for single queries ...or --rlimit-per to use a resource count thus avoiding issues with determinism for multiple runs.
• for Z3 use set_option(timeout=n) to set a global timeout. Alternatively solver objects have a local set method.

Both in milliseconds.

[leonardoalt]

Hi @jmahhh
Thanks!
We're using the C++ APIs, so the z3 option is probably easy to set, but CVC4 doesn't have an API option for that, as far as I know.

[chriseth]

@rofiqgilang note that you cannot use commandline options here, since we use the C / C++ interface to the solvers.

[gitcoinbot]

@rofiqgilang Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@rofiqgilang Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@rofiqgilang due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@vghorakavi Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

@vghorakavi Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[veena-v-g]

Yes I am working on the issue.

[gitcoinbot]

@vghorakavi Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[vs77bb]

@vghorakavi Any update to provide? We may send this back out if we don't hear back soon. Hope you're doing well!

[veena-v-g]

@vs77bb Howdy. Apologies for the late reply.

PR: I have started working with the CVC4 solver. Am not sure how to limit the time spent looking for a solution. I am working on the code in C++. Hope to start working with Z3 soon.

[leonardoalt]

Hi @vghorakavi ,
Z3 has a context option to set the time limit via the API, but CVC4 and SmtLibInteface don't. As described above, the general solution would be a portable code that runs the solver on a separate thread and kills it after the time limit answering Unknown.

[gitcoinbot]

@vghorakavi Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@vghorakavi due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[veena-v-g]

@gitcoinbot This has been done in error. I am still working on the issue. Thank you!

[leonardoalt]

According to https://github.com/CVC4/CVC4/issues/2174 the CVC4 API also has a way to set time limits, so we probably don't need an extra thread.

[vs77bb]

Thanks for the heads up, @vghorakavi 😄

[gitcoinbot]

@vghorakavi Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[gitcoinbot]

Issue Status: 1. Open 2. Started 3. Submitted 4. Done

---

@vghorakavi due to inactivity, we have escalated this issue to Gitcoin's moderation team. Let us know if you believe this has been done in error!

• [x] warning (3 days)
• [x] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[veena-v-g]

Working on understanding CVC4 API. Will submit PR tonight (PR == pull request).

[axic]

@vghorakavi great, thank you!

[axic]

@vs77bb it seems that unfortunately @vghorakavi didn't had time to finish it and one of the Solidity devs was anxious to get it fixed and did it himself 😉

Can the bounty be removed?

[gitcoinbot]

@vghorakavi Hello from Gitcoin Core - are you still working on this issue? Please submit a WIP PR or comment back within the next 3 days or you will be removed from this ticket and it will be returned to an ‘Open’ status. Please let us know if you have questions!

• [x] warning (3 days)
• [ ] escalation to mods (6 days)

Funders only: Snooze warnings for 1 day | 3 days | 5 days | 10 days | 100 days

[vs77bb]

@axic Just notified Greg from MakerDAO to pull the bounty here, thanks for the heads up 🙂

[gitcoinbot]

Issue Status: 1. Open 2. Cancelled

---

__The funding of 150.0 DAI (150.0 USD @ $1.0/DAI) attached to this issue has been cancelled by the bounty submitter__

• Questions? Checkout Gitcoin Help or the Gitcoin Slack
• $28,672.52 more funded OSS Work available on the Gitcoin Issue Explorer