Skip to content

Conversation

@JKTKops
Copy link
Contributor

@JKTKops JKTKops commented Jul 26, 2022

Fixes #3162

Scope:

Add a new option, --smt-retry-limit, which controls how many times we will retry an SMT query that returned Unknown. Previously, we would always retry once.

Estimate:

I think it's done already, but it's unclear where tests for this feature should go (or even if there should be any, as retries were previously untested anyway).


Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@JKTKops
Copy link
Contributor Author

JKTKops commented Jul 26, 2022

Please see the comment on the issue.

@JKTKops JKTKops requested a review from ana-pantilie July 26, 2022 21:00
@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-lemmas.sh 0.000003 -0.004825
test/regression-evm/test-dsvalue-peek-pass-rough.sh 0.000000 0.002053
test/regression-evm/test-storagevar03.sh 0.000007 -0.001172
test/regression-evm/test-totalSupply.sh 0.000009 -0.000618
test/regression-evm/test-addu48u48.sh 0.000003 -0.006357
test/regression-evm/test-sum-to-n.sh 0.000017 0.005982
test/regression-wasm/test-memory.sh 0.000017 0.000000
test/regression-wasm/test-wrc20.sh 0.000015 0.021618
test/regression-wasm/test-simple-arithmetic.sh 0.000011 0.000000
test/regression-wasm/test-locals.sh -0.000000 -0.000000
test/regression-wasm/test-loops.sh 0.000053 -0.000000

@JKTKops JKTKops marked this pull request as ready for review July 27, 2022 02:49
Copy link
Contributor

@ana-pantilie ana-pantilie left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

@ana-pantilie ana-pantilie merged commit 9f7010f into master Jul 27, 2022
@ana-pantilie ana-pantilie deleted the z3-max-retries branch July 27, 2022 04:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Option to adjust the number of solver query retries

3 participants