Regression Bugs + New Support#143
Merged
yannicnoller merged 10 commits intoSymbolicPathFinder:sv-compfrom Feb 26, 2026
Merged
Conversation
Removed hardcoded comment about bitvector length.
RUntime exceptions are printed but the execution does not fail, although it will be flagged as unsafe, and the witness generated will spurious.
I would rather use UnsupportedOperationException but there might be some error checking somewhere that might behave differently. Althought UOE is a type of runtimeexception, will need feedback on this
- refactored the rem overloads in ProblemZ3.java using a conditional If-Then-Else (ITE) block. to negate the dividend to make it positive (aligning with Z3's expected input) - mixed operator in ProblemZ3.java now performs runtime sort-detection for intExpr,RealExpr, or BitVecExpr - patched Edge.java to expand its type-awareness, explicitly adding support for long, short, and byte.
Author
To be more specific here are the benchmarks failing when the mixed operator is not implemented/commented out in my case:
/jpf-regression/ExSymExeD2I_true |
|
@SalmaneKhalili , thank you for your contributions. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Issue
#138
Implementations:
refactored the rem operator in ProblemZ3.java using a conditional If-Then-Else (ITE) block.
Logic: (dividend < 0) ? -(-dividend % divisor) : (dividend % divisor)
by negating the dividend to make it positive we align with Z3's expected input when performing the modulo, and then negating the result back, forces the solver to respect Java's sign convention.
Verdict: New Support for ExSymExeI2D_false.yml + negated some regression tests.
a mixed operator that performs runtime sort-detection and proper casting before executing the operation, which gives us possibility to mix reals, integers, and bitvectors.
Verdict: negated some regression tests.
patched gov.nasa.jpf.symbc.witness.Edge.java to expand its type-awareness, explicitly adding support for long, short, and byte. previously it was hardcoded to deal with only a few types, which would flag an assertion failure and flag ExSymExeLongBytecodes_false and ExSymExeLCMP_false as unknown.
refactored exception messages to be more helpful for future debugging.
Overall results:
jpf-regression benchmarks
Fixed 7 Regression bugs.
Added NEW support for 3 failures.
Benchexec files:
jpf-regression.2026-02-10_11-44-27.results.spf-regression-run.JPF-Regression-Only.txt
Next Todo
Will be addressing jdart-regressions, mainly:
[ ] Add shift support in ProblemZ3, this alone would knock out 3 regression tests in jdart-regression sv-benchmarks.
[ ] Look into D2L, i believe we have lossy conversion making us fail jdart-regression/double2long.yml
[ ] add radians to our overwritten native math library for jdart-regression/radians.yml