Skip to content

Add common optimization prover delegate#671

Merged
baierd merged 6 commits into
masterfrom
add_common_optimizationProver_delegate2
Jun 12, 2026
Merged

Add common optimization prover delegate#671
baierd merged 6 commits into
masterfrom
add_common_optimizationProver_delegate2

Conversation

@baierd

@baierd baierd commented Jun 9, 2026

Copy link
Copy Markdown
Contributor

This PR extracts common checks of OptimizationProverEnvironments into a single new delegate OptimizationProverDelegate.

Changes:

  • fixes a bug in Z3. In certain cases it was possible to request a model even if the preconditions were not fulfilled.

daniel-raffler
daniel-raffler previously approved these changes Jun 12, 2026

@daniel-raffler daniel-raffler left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM

Comment thread src/org/sosy_lab/java_smt/basicimpl/OptimizationProverDelegate.java
@baierd baierd merged commit 8a91a7f into master Jun 12, 2026
19 of 21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Development

Successfully merging this pull request may close these issues.

2 participants