Skip to content

Small bugfix in compute_sibling_resolvent#8031

Merged
NikolajBjorner merged 110 commits intoZ3Prover:parallelfrom
ilanashapiro:param-tuning
Nov 17, 2025
Merged

Small bugfix in compute_sibling_resolvent#8031
NikolajBjorner merged 110 commits intoZ3Prover:parallelfrom
ilanashapiro:param-tuning

Conversation

@ilanashapiro
Copy link
Copy Markdown
Contributor

I was making my slides for my talk this week and going through the search_tree.h code I think I may have found a small bug in compute_sibling_resolvent

ilanashapiro and others added 30 commits September 30, 2025 11:35
Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](actions/checkout@v4...v5)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: '5'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
… different threads don't interfere (Z3Prover#7963)

* Initial plan

* Add mutex to warning.cpp for thread safety

Co-authored-by: NikolajBjorner <[email protected]>

---------

Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: NikolajBjorner <[email protected]>
Removed unused variable 'first' from the function.
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
ilanashapiro and others added 27 commits October 30, 2025 22:17
Signed-off-by: Nikolaj Bjorner <[email protected]>
…uners or it spins infinitely. added flag for this. but now there is segfault on the probe_ctx.check() call
* Initial plan

* Add C API and Java bindings for str.replace_all, str.replace_re, str.replace_all_re

Co-authored-by: NikolajBjorner <[email protected]>

* Add test for new Java string replace operations

Co-authored-by: NikolajBjorner <[email protected]>

* Remove author field from test file header

Co-authored-by: NikolajBjorner <[email protected]>

* Delete examples/java/StringReplaceTest.java

---------

Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: NikolajBjorner <[email protected]>
Co-authored-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
…param tuning experiments on QF_RDL. set up this logic in the smt_parallel files
…ew user param to toggle for only running param tuning thread without parallel solving (just to test if it's finding good settings)
@NikolajBjorner NikolajBjorner merged commit abbbc3c into Z3Prover:parallel Nov 17, 2025
1 check passed
@NikolajBjorner
Copy link
Copy Markdown
Contributor

somehow search_tree in this branch is based on an older version than search_tree.h in the master branch.
I didn't find the bug in the master branch.
Perhaps update search_tree to be more current?

@ilanashapiro
Copy link
Copy Markdown
Contributor Author

I believe we added the optimization here about pruning the tree via resolving cores upward? I don't think that exists on the master branch yet (started with this commit 52fd59d and ended with this commit c5d65cd)

the master branch just has close_node, vs parallel now has close_with_core

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.

6 participants