Skip to content

Conversation

@wadoon
Copy link
Member

@wadoon wadoon commented Dec 30, 2025

Related Issue

The broad release tests are currently failing on macOS.

  • This PR updates the workflow "Broad Release Tests" by adding more variants and executing the SMT tests with different Z3/CVC5 versions.

  • On https://github.com/keyproject/setup-smt was updated to version 0.3.0

  • "Optional Tests" had a bug with colon in artifact name.

  • Clean up of .github older.

Testing is only possible after the merge or on your own fork.

Plan

  • Fix the Optional Tests (aka key.core.proof_references and key.core.symbolic_execution)

    I activated these tests in the broad release tests, when we release everything should be accurate. 
    
  • Artifact name clash for integration tests

Error: Failed to CreateArtifact: Received non-retryable error: Failed request: (409) Conflict: an artifact with this name already exists on the workflow run

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • There are changes to the deployment/CI infrastructure (gradle, github, ...)

Ensuring quality

@wadoon wadoon added this to the v2.13.0 milestone Dec 30, 2025
@wadoon wadoon requested a review from unp1 December 30, 2025 06:51
@wadoon wadoon self-assigned this Dec 30, 2025
@wadoon wadoon added the 🛠 Maintenance Code quality and related things w/o functional changes label Dec 30, 2025
@wadoon wadoon force-pushed the weigl/broad-release-tests branch from cd0f34d to 90b2e1c Compare December 30, 2025 06:58
@wadoon wadoon requested a review from mattulbrich December 30, 2025 06:58
@wadoon wadoon marked this pull request as ready for review December 30, 2025 06:58
@wadoon
Copy link
Member Author

wadoon commented Dec 30, 2025

@mattulbrich The tests testProveSMTLemmas and testStrictSMT were added to the Broad Release Tests. Does it make sense to test them under different SMT solvers? Do we have a test suite for SMT-dependent tests?

@WolframPfeifer WolframPfeifer modified the milestones: v2.13.0, v3.0.0 Jan 7, 2026
Copy link
Member

@unp1 unp1 left a comment

Choose a reason for hiding this comment

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

looks fine

colon not allowed in artifact names
* setup-smt updated to version 0.3.0 to support more z3/cvc5 versions
* executes the smt tests
* execute tests with different z3/cvc5 on different platform for
  different java versions

# Conflicts:
#	.github/workflows/sonarqube.yml
#	.github/workflows/tests_winmac.yml
@wadoon wadoon force-pushed the weigl/broad-release-tests branch from 040411a to ebdca3f Compare January 13, 2026 22:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

🛠 Maintenance Code quality and related things w/o functional changes

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants