Skip to content

Conversation

@FliegendeWurst
Copy link
Member

CVC5 now also supports printing unsat cores, cvc5/cvc5#9353 has been released for years.

Intended Change

Enable "Focus goals" function for CVC5.

Type of pull request

  • New feature (non-breaking change which adds functionality)
  • There are changes to the (Java) code
  • Other: changes to the SMT properties

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments): javadoc updated
  • I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs). Currently none of the user-facing SMT functions are documented
  • I added new test case(s) for new functionality. SMT tests are currently being reworked SMT test cases rework #3592
  • I have tested the feature as follows: Open Aunt Agatha, run SMT preparation, run CVC5, click "Focus goals". Hides three formulas.
  • I have checked that runtime performance has not deteriorated: unsat core production has been turned on already, printing it should not take long.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@codecov
Copy link

codecov bot commented Apr 11, 2025

Codecov Report

Attention: Patch coverage is 0% with 1 line in your changes missing coverage. Please review.

Project coverage is 39.51%. Comparing base (c14cabc) to head (441d388).
Report is 27 commits behind head on main.

Files with missing lines Patch % Lines
.../de/uka/ilkd/key/smt/communication/CVC5Socket.java 0.00% 1 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff              @@
##               main    #3594      +/-   ##
============================================
+ Coverage     38.57%   39.51%   +0.94%     
- Complexity    17358    17729     +371     
============================================
  Files          2103     2103              
  Lines        127655   127670      +15     
  Branches      21499    21500       +1     
============================================
+ Hits          49240    50449    +1209     
+ Misses        72353    71031    -1322     
- Partials       6062     6190     +128     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

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

Thanks! It is indeed a good idea to enable unsat cores also for cvc5 now.

I first thought about setting the minimum required version to the one with the fix, but I think that is not even necessary, since I changed the solver parameters recently to include --no-interactive (#3593), which should even eliminate the need for this fix at all. @FliegendeWurst Is this correct?

@WolframPfeifer WolframPfeifer added SMT Feature New feature or request labels Apr 15, 2025
@FliegendeWurst
Copy link
Member Author

I think so, going by my bug report to CVC5 (cvc5/cvc5#9350). The issue only occured with --interactive.

@wadoon wadoon added this pull request to the merge queue Apr 15, 2025
Merged via the queue into KeYProject:main with commit e36d6a4 Apr 15, 2025
7 of 9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Feature New feature or request SMT

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants