Repository navigation

SV-COMP 2027 version - #92

Merged

nils-loose merged 264 commits into

devfrom

chore/dependency-update

Oct 20, 2026

Merged

SV-COMP 2027 version#92
nils-loose merged 264 commits into
devfrom
chore/dependency-update

This pull request is big! We're only showing the most recent 250 commits

Commits on Sep 2, 2026
- Fix --no-sa option
  solid-eureka
  committed
  bc73864
Commits on Sep 3, 2026
- Enhance logging for static pre-analysis and update config file handling in sv-comp
  solid-eureka
  committed
  207d6a7
- Refactor SANode and add exceptional child handling
  solid-eureka
  committed
  27e5a11
Commits on Sep 4, 2026
- Remove duplicate call to checkAndSetBranch in visitIF_ACMPEQ
  solid-eureka
  committed
  84cc7d0
Commits on Sep 7, 2026
- Add more SA stats logging
  solid-eureka
  committed
  9c8047e
- TEST: Prevent false SAFE classifications.
  solid-eureka
  committed
  e77bddb
Commits on Sep 8, 2026
- Log current commit when running sv-comp
  solid-eureka
  committed
  a88eb78
- Use different strategy of preventing false SAFE classifications
  solid-eureka
  committed
  e8c0e4f
Commits on Sep 10, 2026
- Add shorthand notation for comparing results
  solid-eureka
  committed
  ee415f4
- Add allowlist for class names beginning with 'L'
  solid-eureka
  committed
  7da5083
- Improve run analysis: Output performance metrics and merge similar errors
  solid-eureka
  committed
  9872c26
- Fix SMT solver timing and split out static pre-analysis stage
  
  solid-eureka
  and
  claude
  committed
  466cafc
- Cleanup debug code in SolverHandler.py
  solid-eureka
  committed
  4c101c7
Commits on Sep 19, 2026
- Add --sa-retry-without option to gate failsafe behavior
  solid-eureka
  committed
  33ad778
- Implement StringValue.invokeIsEmpty()
  solid-eureka
  committed
  18f2003
Commits on Sep 21, 2026
- Pass absolute classpath to CFG extractor
  
  solid-eureka
  and
  claude
  committed
  9fd6bd7
- Add virtual dispatch example
  solid-eureka
  committed
  a026a54
- Skip SA branch traversal inside static initializer blocks
  solid-eureka
  committed
  fab078a
- Use logger for DFS
  solid-eureka
  committed
  3895cc9
- Increase SA timeout for SVComp
  solid-eureka
  committed
  a5b6b6f
Commits on Sep 22, 2026
- Update notes
  solid-eureka
  committed
  b40b409
Commits on Sep 24, 2026
- Add timeout option to SVComp script
  solid-eureka
  committed
  c98ded0
- Improve error reporting for loading SA graphs
  solid-eureka
  committed
  e45ea2c
- Fix SA graph traversal in DFS
  solid-eureka
  committed
  284b967
- Update handling of incomplete SA graphs
  solid-eureka
  committed
  5cc7462
- Log argv when running SVComp
  solid-eureka
  committed
  20183dd
Commits on Sep 26, 2026
- Consistent case_occurrences order in results.json files
  solid-eureka
  committed
  f671352
- Stop echoing logs in parallel SVComp runs
  solid-eureka
  committed
  d1fccf9
Commits on Sep 27, 2026
- Walk the static-analysis graph with a call stack
  
  solid-eureka
  and
  claude
  committed
  2780fc3
- Add CLAUDE.md
  solid-eureka
  committed
  7f56b54
- Stop printing the whole tree when running SAGraph.py directly
  solid-eureka
  committed
  0f1fff8
- WIP: Runtime comparison plots
  solid-eureka
  committed
  7c54640
- More runtime comparison plots
  solid-eureka
  committed
  dd454f6
- Runtime plots as SVG
  solid-eureka
  committed
  42e842c
- Improve plot script ease-of-use
  solid-eureka
  committed
  58f2291
Commits on Sep 28, 2026
- Add plot showing results as if static pre-analysis took no time
  solid-eureka
  committed
  cc7f1eb
- Add support for linear plots
  solid-eureka
  committed
  1610bbc
- Run static pre-analysis in the background during exploration
  
  solid-eureka
  and
  claude
  committed
  1a5c545
Commits on Sep 29, 2026
- Rank branches by distance to an assert (--sa-rank-distance)
  
  solid-eureka
  and
  claude
  committed
  51d57d5
- Encode char inputs as numbers
  
  solid-eureka
  and
  claude
  committed
  a0eba44
- Parse negative long inputs
  
  solid-eureka
  and
  claude
  committed
  52679a0
- Model Character predicates and case mappings
  
  solid-eureka
  and
  claude
  committed
  434f262
- Model String trim, compareTo, lastIndexOf, regionMatches and valueOf(Object)
  
  solid-eureka
  and
  claude
  committed
  a99050e
- Model Math floor/ceil/rint/toRadians/toDegrees/getExponent exactly and pow/tan/atan/log/exp/... by sampling
  
  solid-eureka
  and
  claude
  committed
  984b3bd
- Record bounds checks of untracked arrays as concrete-only branches
  
  solid-eureka
  and
  claude
  committed
  04a6413
- Record context loss when an uninstrumented call with symbolic arguments throws
  
  solid-eureka
  and
  claude
  committed
  5ea26bc
- Wait for static pre-analysis by default; add --parallel-sa
  
  solid-eureka
  and
  claude
  committed
  6646e78
- Remove notes
  solid-eureka
  committed
  4675078
- Log divergences from approximate-model solutions as expected
  
  solid-eureka
  and
  claude
  committed
  15f0893
Commits on Sep 30, 2026
- Add --solver-rlimit: escalating Z3 resource limits per branch
  
  solid-eureka
  and
  claude
  committed
  b3d687c
- Switch to the latest SV-Benchmarks and keep the old suite
  
  solid-eureka
  and
  claude
  committed
  6e087b8
- Note the local label fix for ReverseInterpolator_true
  
  solid-eureka
  and
  claude
  committed
  0a7e127
Commits on Oct 1, 2026
- Note the local label fixes for PieSegment_true and AlbersProjection_true
  
  solid-eureka
  and
  claude
  committed
  b7ae54f
Commits on Oct 14, 2026
- Fix log paths for --benchmark-dir with other folder names
  
  solid-eureka
  and
  claude
  committed
  939933e
- Add swat-benchmarks: pruning benefit families and SA soundness pairs
  
  solid-eureka
  and
  claude
  committed
  4328048
- swat-benchmarks: add narrowing tasks for SA and executor false SAFEs
  
  solid-eureka
  and
  claude
  committed
  8bf59a1
- swat-benchmarks: add real-tools harnesses (getopt, opencsv) and report script
  
  solid-eureka
  and
  claude
  committed
  fcb2aa6
- swat-benchmarks: add README and results write-up
  
  solid-eureka
  and
  claude
  committed
  92fc813
- Mention swat-benchmarks in CLAUDE.md
  
  solid-eureka
  and
  claude
  committed
  289f411
Commits on Oct 15, 2026
- RESULTS.md: count family and soundness false SAFEs separately
  
  solid-eureka
  and
  claude
  committed
  563bd52
- CLAUDE.md: note that asserts are only the first pruning target
  
  solid-eureka
  and
  claude
  committed
  38ac0b7
- build: make SV-COMP archive run on Ubuntu 26.04 (SV-COMP 2027)
  
  nils-loose
  and
  claude
  committed
  e343ec1
- Emit YAML violation witnesses (format 2.3) for SV-COMP 2027
  
  nils-loose
  and
  claude
  committed
  737f96e
- CLAUDE.md: note the deferred trace-event and id-pairing redesign
  
  solid-eureka
  and
  claude
  committed
  bb8ff31
- Send the trace before System.exit, Runtime.exit and Runtime.halt in SV-COMP mode
  
  solid-eureka
  and
  claude
  committed
  90fd881
- Track non-capturing lambda bodies; record context loss when instrumented code runs untracked
  
  solid-eureka
  and
  claude
  committed
  b67695d
- Keep symbolic arguments of Method.invoke: unbox them, handle static targets, check Object[] args
  
  solid-eureka
  and
  claude
  committed
  45c2cd6
- Record precision loss for symbolic indices into object or untracked arrays
  
  solid-eureka
  and
  claude
  committed
  d612f78
- Pass solved inputs back by name, ignoring symbolic values that are no Verifier input
  
  solid-eureka
  and
  claude
  committed
  b6573fb
- Keep String inputs within Java chars and pass them back exactly
  
  solid-eureka
  and
  claude
  committed
  16303f1
- Do not count constraints over String inputs as precision loss
  
  solid-eureka
  and
  claude
  committed
  afbd1db
- Follow the NullPointerException of a field access on null instead of halting
  
  solid-eureka
  and
  claude
  committed
  3b2b979
- Close static initializers left by an exception before the invoke below them ends
  
  solid-eureka
  and
  claude
  committed
  f1ee845
- Merge remote-tracking branch 'origin/feat/yaml-witnesses' into feat/witness-via-trace
  nils-loose
  committed
  b14fdaf
- Ship witness data in the trace instead of stdout markers
  
  nils-loose
  and
  claude
  committed
  7430bef
- Write SV-COMP violation witnesses from the trace via witnesscreator
  
  nils-loose
  and
  claude
  committed
  feaa359
- Package witnesscreator instead of the WitnessCreator jar
  
  nils-loose
  and
  claude
  committed
  39188f8
- Validate the explorer-written witnesses in the local harness
  
  nils-loose
  and
  claude
  committed
  be5ddca
- Record the calling method and send the trace on System.exit
  
  nils-loose
  and
  claude
  committed
  f18d36f
Commits on Oct 16, 2026
- Model StringBuilder.setLength for concrete lengths
  
  solid-eureka
  and
  claude
  committed
  1a05ac4
- swat-benchmarks: add StringBuilder.setLength reproducer
  
  solid-eureka
  and
  claude
  committed
  6bbd2b8
- CLAUDE.md: note String input escaping and the new soundness flags
  
  solid-eureka
  and
  claude
  committed
  1736b17
- Give every String input its own object, so equal inputs keep separate variables
  
  solid-eureka
  and
  claude
  committed
  5c0fdec
- Model String.indexOf(String, int) with Java's clamping of fromIndex
  
  solid-eureka
  and
  claude
  committed
  34cd826
- Report UNKNOWN instead of SAFE after a solution did not reach its branch
  
  solid-eureka
  and
  claude
  committed
  18b0af7
- swat-benchmarks: add reproducers for equal String inputs and indexOf with negative fromIndex
  
  solid-eureka
  and
  claude
  committed
  6357110
- Find the target of a divergence check by its position, not by its (repeatable) id
  
  solid-eureka
  and
  claude
  committed
  fc8e88e
- RESULTS.md: add the fixes of 2026-10-15/16 and the runs after them
  
  solid-eureka
  and
  claude
  committed
  71dc9cb
- SA graph: model exceptions of unknown type (pseudo types caught by any listed handler)
  
  solid-eureka
  and
  claude
  committed
  9ce3d15
- Stop trusting the SA graph after an exception it does not model
  
  solid-eureka
  and
  claude
  committed
  552bcc0
- Close a static initializer left by an exception once the frame below it continues
  
  solid-eureka
  and
  claude
  committed
  86c0da2
- swat-benchmarks: add S2 reproducers (callee-decided NPE, Error from an initializer, finally)
  
  solid-eureka
  and
  claude
  committed
  f0ccb96
- Document the S2 fix (unmodelled exceptions) in CLAUDE.md and RESULTS.md
  
  solid-eureka
  and
  claude
  committed
  fce1bec
- swat-benchmarks: add exception-dispatch family (SA precision after unmodelled exceptions)
  
  solid-eureka
  and
  claude
  committed
  1e6cdea
- Executor: record HANDLER_ENTRY events
  
  solid-eureka
  and
  claude
  committed
  6fb7464
- SA walk: resume at the handler after an unmodelled exception
  
  solid-eureka
  and
  claude
  committed
  50ce3ff
- sa-soundness: handler resumption tasks
  
  solid-eureka
  and
  claude
  committed
  7f6aa4c
- Docs: handler resumption results
  
  solid-eureka
  and
  claude
  committed
  b3a08e7
Commits on Oct 17, 2026
- Executor: report branch keys and stack changes in the trace
  
  solid-eureka
  and
  claude
  committed
  1568fec
- SA walk: detect desyncs by key and resync after losing the graph
  
  solid-eureka
  and
  claude
  committed
  fc817ee
- Docs: branch keys, desync detection and resync
  
  solid-eureka
  and
  claude
  committed
  66a5d02
- Remove handler resumption (covered by resync)
  
  solid-eureka
  and
  claude
  committed
  8f5505e
- Mask library callbacks in the SA walk
  
  solid-eureka
  and
  claude
  committed
  aa20dab
- sa-soundness: library callback tasks; docs
  
  solid-eureka
  and
  claude
  committed
  8dab346
- sa-soundness: library-callback-assert (known false SAFE with SA)
  
  solid-eureka
  and
  claude
  committed
  d8289a7
- Flag to turn off callback targets (--sa-no-callback-targets)
  
  solid-eureka
  and
  claude
  committed
  6ced24e
- Key the solver's constraint cache by tree node, not iid
  
  solid-eureka
  and
  claude
  committed
  f6197d3
- sa-soundness: exec-loop-iid-wrap
  
  solid-eureka
  and
  claude
  committed
  9046cd0
- Keep Z3's jar off the extractor's classpath
  
  solid-eureka
  and
  claude
  committed
  69c6b83
- SA walk: call sites with several callees (union in summaries, resync inside)
  
  solid-eureka
  and
  claude
  committed
  98eb95d
- Docs: callback targets, multi-target calls, solver cache fix
  
  solid-eureka
  and
  claude
  committed
  65aab6e
- Remove dead code left from the SA integration
  
  solid-eureka
  and
  claude
  committed
  604ba0a
- Remove generated timing plot, ignore it
  
  solid-eureka
  and
  claude
  committed
  8f0501b
Commits on Oct 18, 2026
- Merge remote-tracking branch 'origin/feat/witness-via-trace' into svcomp27/integration
  nils-loose
  committed
  2f8e874
- Merge #65 (static pre-analysis) into the integration branch
  
  nils-loose
  and
  claude
  committed
  e65dbe2
- Static pre-analysis: prune only under valid-assert and within main's call tree
  
  nils-loose
  and
  claude
  committed
  f948cb0
- SA walk: do not prune at a branch whose pairing could not be checked
  
  nils-loose
  and
  claude
  committed
  6eb7bff
- Tests for the pre-analysis guards and unchecked pairings
  
  nils-loose
  and
  claude
  committed
  aa8a0ef
- Encode NaN and signed zeros in FCMPG/FCMPL
  
  nils-loose
  and
  claude
  committed
  45addc3
- Support Verifier.nondetObject in the SV-COMP instrumentation
  
  nils-loose
  and
  claude
  committed
  896cab9
- Re-solve a branch whose solution's run does not reach it
  
  nils-loose
  and
  claude
  committed
  8f78f91
- Release the Database lock on exceptions and record traces that cannot be added
  
  nils-loose
  and
  claude
  committed
  42ac10b
- End a failed or incomplete SV-COMP run with UNKNOWN
  
  nils-loose
  and
  claude
  committed
  f83326f
- Extract constraint variables without recursion, each subterm once
  
  nils-loose
  and
  claude
  committed
  58c15ae
- Build and walk the execution tree iteratively; keep UNMODELLED_EXCEPTION off its levels
  
  nils-loose
  and
  claude
  committed
  373384d
- Make the class name check descriptor-aware
  
  nils-loose
  and
  claude
  committed
  e9ae9b0
- Add a static check for uncaught RuntimeExceptions and AssertionErrors
  
  nils-loose
  and
  claude
  committed
  508db53
- Answer SAFE when the property pre-check proves the property
  
  nils-loose
  and
  claude
  committed
  2273466
- Test the property pre-check and the verdict it gives
  
  nils-loose
  and
  claude
  committed
  c41571f
- Check only the static initializers that may run
  
  nils-loose
  and
  claude
  committed
  3445d64
- Continue the running symbolic execution in nested endpoints
  
  nils-loose
  and
  claude
  committed
  eaeb2d9
- Start the symbolic execution in the entry class's static initializer
  
  nils-loose
  and
  claude
  committed
  b09b432
- Close soundness gaps in the exception-freedom check
  
  nils-loose
  and
  claude
  committed
  d0d7357
- Report an assertion failure where its AssertionError is thrown
  
  nils-loose
  and
  claude
  committed
  de4930b
- Branch on the element a symbolic index selects in an object array
  
  nils-loose
  and
  claude
  committed
  cfdc451
- Hold the SA walk in place over choice branches
  
  nils-loose
  and
  claude
  committed
  cbd98d0
- Test the object-array index search in a forked agent
  
  nils-loose
  and
  claude
  committed
  9f0306e
- Decide precision loss by symbol kind instead of by name
  
  nils-loose
  and
  claude
  committed
  f55b477
- Declare the approximate UF models and record their precision loss
  
  nils-loose
  and
  claude
  committed
  db4cd1e
- Model Integer/Long bit operations and radix-2^k string conversions
  
  nils-loose
  and
  claude
  committed
  edf7764
- Fix Short.compareUnsigned model to return the difference
  
  nils-loose
  and
  claude
  committed
  31aab84
- Model Double.doubleToLongBits/doubleToRawLongBits, canonicalise NaN bits
  
  nils-loose
  and
  claude
  committed
  cf03553
- Add spec comparing Integer/Long/Short/Byte/Double/Float models with the JDK
  
  nils-loose
  and
  claude
  committed
  4ce61c0
- Return a concrete result from Objects.equals with a null operand
  
  nils-loose
  and
  claude
  committed
  506c20b
- Reproduce Java reference identity in the IF_ACMP rewrite
  
  nils-loose
  and
  claude
  committed
  0152059
- Downgrade SAFE on a reference semantic change
  
  nils-loose
  and
  claude
  committed
  6d51129
- Treat calls that a library default method may serve as unknown
  
  nils-loose
  and
  claude
  committed
  1675424
- Model Math.round, max/min, signum, floorDiv and floorMod exactly
  
  nils-loose
  and
  claude
  committed
  9358459
- Model transcendental Math calls as per-call uninterpreted functions
  
  nils-loose
  and
  claude
  committed
  adebf40
- Slice UF definitions per query and bound queries over Math models
  
  nils-loose
  and
  claude
  committed
  7141297
- Handle a StackOverflowError in the target as the plain JVM would
  
  nils-loose
  and
  claude
  committed
  ae1b9e5
- Do not report a violation of an execution that overflowed the stack
  
  nils-loose
  and
  claude
  committed
  db097ce
- Build comparison results and Integer-to-bit-vector conversions over bit-vectors
  
  nils-loose
  and
  claude
  committed
  22dce63
- Skip functions when reading input values from a model
  
  nils-loose
  and
  claude
  committed
  cba8042
- Lower the default resource limit for queries over Math models to 2.5e8
  
  nils-loose
  and
  claude
  committed
  a33984a
- Encode bit-op and radix-string models without shared subterms
  
  nils-loose
  and
  claude
  committed
  a8c403c
- Model reference-only calls on JDK containers
  
  nils-loose
  and
  claude
  committed
  c2a4c50
- Make the String models match Java
  
  nils-loose
  and
  claude
  committed
  0f84f31
- Make the StringBuilder model exact, and record the index checks of String calls
  
  nils-loose
  and
  claude
  committed
  186d971
- Do not count the exactly defined String UFs as precision loss
  
  nils-loose
  and
  claude
  committed
  ae83736
- Test that the String and StringBuilder models are exact
  
  nils-loose
  and
  claude
  committed
  0df4738
- Model System.arraycopy with concrete positions and length
  
  nils-loose
  and
  claude
  committed
  1bca0a5
- Test the JDK container and arraycopy models
  
  nils-loose
  and
  claude
  committed
  5a33932
- Solve comparisons over int_to_bv of string lengths and char codes over the Integers
  
  nils-loose
  and
  claude
  committed
  634d6f7
- Extract constraint variables without recursion, each subterm once
  
  nils-loose
  and
  claude
  committed
  5d7de94
- Add choice branches: executor-added branches that enumerate an operand's values
  
  nils-loose
  and
  claude
  committed
  ee59502
- Model Integer/Long toString and toUnsignedString with a radix
  
  nils-loose
  and
  claude
  committed
  4c79e69
- Fix the string of a negative long or short in concatenation
  
  nils-loose
  and
  claude
  committed
  3c8ea30
- Convert floats and doubles to their concrete string
  
  nils-loose
  and
  claude
  committed
  b701046
- Solve program branches before choice branches
  
  nils-loose
  and
  claude
  committed
  f4486e3
- Remove the unused SVCompHandler
  
  nils-loose
  and
  claude
  committed
  942d66d
- Keep SV-COMP runs within the competition's memory and CPU budget
  
  nils-loose
  and
  claude
  committed
  a863ff5
- Test the number-to-string models against the JDK
  
  nils-loose
  and
  claude
  committed
  2b6ba31
- Run the executor JVM with the C1 compiler only
  
  nils-loose
  and
  claude
  committed
  0269e0b
- Use the same resource budget in the competition package and the harness
  
  nils-loose
  and
  claude
  committed
  a1c072c
- Do not close the solver context at the end of an SV-COMP execution
  
  nils-loose
  and
  claude
  committed
  ab37625
- Encode the trace with one Z3 solver for all formulas, compact JSON
  
  nils-loose
  and
  claude
  committed
  f67f39d
- Create the solver contexts with java-smt's null log manager
  
  nils-loose
  and
  claude
  committed
  d1ac405
- Run the executor JVM with C1 only
  
  nils-loose
  and
  claude
  committed
  2dcd94c
- Select the next branch without copying the execution tree
  
  nils-loose
  and
  claude
  committed
  e4305de
- Keep the nested replace, as precision loss; model the constructor's capacity
  
  nils-loose
  and
  claude
  committed
  ac1a353
- Fail the check when the JVM would not load the classpath as modelled
  
  nils-loose
  and
  claude
  committed
  9cd00a6
- Stop growing ClassDepot's cached hierarchy lists on every allocation
  
  nils-loose
  and
  claude
  committed
  ccd0536
- Look up the reflected field by its name in Field.get
  
  nils-loose
  and
  claude
  committed
  1624541
- Store String[] rows created by ANEWARRAY into multi-dimensional arrays
  
  nils-loose
  and
  claude
  committed
  81f8042
- Close constructor invokes left by an exception inside a constructor
  
  nils-loose
  and
  claude
  committed
  30be08f
- Resync a diverged primitive value with a context loss instead of halting
  
  nils-loose
  and
  claude
  committed
  519c375
- Convert floats and doubles to strings concretely
  
  nils-loose
  and
  claude
  committed
  3ee3cb4
- Add agent tests for entry-method start, nested mains and constructor exceptions
  
  nils-loose
  and
  claude
  committed
  f6c0a51
- Encode NaN and signed zeros in FCMP and the compare/compareTo models
  
  nils-loose
  and
  claude
  committed
  339a71c
- Recheck only mutable map keys for symbolic state
  
  nils-loose
  and
  claude
  committed
  a5740d7
- Merge remote-tracking branch 'origin/fix/exit-hides-assertion' into svcomp27/all-fixes
  nils-loose
  committed
  db0fff1
- Merge remote-tracking branch 'origin/fix/sa-property-guard' into svcomp27/all-fixes
  nils-loose
  committed
  acd18e3
- Merge remote-tracking branch 'origin/fix/uf-detection-by-kind' into svcomp27/all-fixes
  nils-loose
  committed
  d0addcf
- Merge remote-tracking branch 'origin/feat/property-aware-downgrade' into svcomp27/all-fixes
  nils-loose
  committed
  d7841dc
- Merge remote-tracking branch 'origin/feat/collections-jdk-models' into svcomp27/all-fixes
  nils-loose
  committed
  dc34189
- Merge feat/symbolic-object-array-index (#69) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  b1db004
- Count each stop of the resource budget once
  
  nils-loose
  and
  claude
  committed
  08fcd4e
- Merge feat/number-to-string-models (#76, includes #70) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  a5b76de
- Report loop-head states with the trace
  
  nils-loose
  and
  claude
  committed
  98e402a
- Leave out branches below a repeated loop-head state
  
  nils-loose
  and
  claude
  committed
  1a4e046
- Enable loop-state matching in the SV-COMP configuration
  
  nils-loose
  and
  claude
  committed
  b138c9d
- Bound the time a run spends on loop-head states
  
  nils-loose
  and
  claude
  committed
  44a5a24
- Merge fix/explorer-robustness (#72) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  6ce97bf
- Give the driver robustness tests a property pre-check
  
  nils-loose
  and
  claude
  committed
  92e8fd1
- Merge feat/diverged-branch-retry (#74) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  67d6dbe
- Adapt the divergence and driver tests to the combined driver
  
  nils-loose
  and
  claude
  committed
  f5eeefb
- Merge fix/string-model-soundness (#75) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  cae0290
- Merge fix/stackoverflow-handling (#78) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  358e06f
- Keep a stack overflow of a trace that could not be added
  
  nils-loose
  and
  claude
  committed
  f6624c6
- Merge fix/ref-equality-semantics (#79) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  d1f7ad6
Commits on Oct 19, 2026
- Test variable extraction on shared and deep constraint terms
  
  nils-loose
  and
  claude
  committed
  d757d7f
- End the run when a Z3 query outgrows the memory budget
  
  nils-loose
  and
  claude
  committed
  929b11a
- Merge feat/math-models (#80) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  a29e2b5
- Declare the sampled Math functions as approximate model functions
  
  nils-loose
  and
  claude
  committed
  5c2225e
- Merge perf/solver-encoding (#81) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  65fdc4b
- Merge perf/round-overhead (#82) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  1f5f3b0
- See a given-up branch's later-reached side on the tree's node
  
  nils-loose
  and
  claude
  committed
  f262d4d
- Model StringBuffer, case mappings, ignore-case comparisons and simple regexes exactly
  
  nils-loose
  and
  claude
  committed
  fbea4c1
- Model parsing numbers from Strings exactly, with NumberFormatException as a branch
  
  nils-loose
  and
  claude
  committed
  80ce0f0
- Test that the number parsing models are exact
  
  nils-loose
  and
  claude
  committed
  8f36a25
- Merge feat/parse-number-models (#83, based on #75) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  d80f610
- Count the CPU time of the whole cgroup against the budget
  
  nils-loose
  and
  claude
  committed
  925ce9e
- Log the per-node trace of the branch selection below DEBUG
  
  nils-loose
  and
  claude
  committed
  80287c7
- Pass the explorer's output through in run_swat.py
  
  nils-loose
  and
  claude
  committed
  3e3d367
- Model case mappings and ignore-case comparisons for ASCII strings only
  
  nils-loose
  and
  claude
  committed
  ef7c0ac
- Keep the module loggers' DEBUG/INFO lines off stdout in sv-comp mode
  
  nils-loose
  and
  claude
  committed
  d6a6d21
- Count a symbolic array length as symbolic
  
  nils-loose
  and
  claude
  committed
  22e3844
- Stop reporting loop states after a call into untracked code
  
  nils-loose
  and
  claude
  committed
  ca0f2a5
- Add loop-state matching soundness tasks
  
  nils-loose
  and
  claude
  committed
  730db3a
- Report UNKNOWN for an SV-COMP round in which the target sent no trace
  
  nils-loose
  and
  claude
  committed
  637b685
- Add an end-to-end test for targets that fail before main
  
  nils-loose
  and
  claude
  committed
  008110b
- Cover the competition package wrapper in the failed-start test
  
  nils-loose
  and
  claude
  committed
  193fc2b
- Merge fix/executor-small-bugs (#86) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  4977c74
- Leave toLowerCase/toUpperCase of symbolic strings unmodelled; pin before the ASCII split
  
  nils-loose
  and
  claude
  committed
  bf21183
- Merge fix/resource-budget (#88) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  0b601b2
- Give the driver tests the resource budget and the Database reads
  
  nils-loose
  and
  claude
  committed
  403985d
- Merge fix/failed-start-unknown (#89) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  0ff4068
- Report UNKNOWN for a failed start also when the pre-check proved the property
  
  nils-loose
  and
  claude
  committed
  afd150f
- Test equalsIgnoreCase of two symbolic strings under its branches
  
  nils-loose
  and
  claude
  committed
  29b8c03
- Merge feat/string-models-2 (#90, based on #75) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  c373130
- Mark the number-parsing branches as checks or splits
  
  nils-loose
  and
  claude
  committed
  4b33c36
- Merge feat/loop-state-matching (#84) into svcomp27/all-fixes
  
  nils-loose
  and
  claude
  committed
  d1b8fb8
- Prune only the dominated subtree in the iterative walk; attach loop states to every branch
  
  nils-loose
  and
  claude
  committed
  c89050b
Commits on Oct 20, 2026
- Update Z3 to 5.3.1 in the executor and the explorer
  
  nils-loose
  and
  claude
  committed
  54a2c21
- Update ASM, Jackson, logback, SLF4J, Spock and Mockito
  
  nils-loose
  and
  claude
  committed
  09c4552
- Update Gradle to 8.14.6 and the build plugins
  
  nils-loose
  and
  claude
  committed
  0fc33f3
- Update the Python dependencies
  
  nils-loose
  and
  claude
  committed
  5cdec5c
- Update the GitHub Actions used by CI
  
  nils-loose
  and
  claude
  committed
  57413b5
- Keep Z3's previous regex solver in the explorer
  
  nils-loose
  and
  claude
  committed
  f2d8115

Commits

Commits on Sep 2, 2026

Commits on Sep 3, 2026

Commits on Sep 4, 2026

Commits on Sep 7, 2026

Commits on Sep 8, 2026

Commits on Sep 10, 2026

Commits on Sep 19, 2026

Commits on Sep 21, 2026

Commits on Sep 22, 2026

Commits on Sep 24, 2026

Commits on Sep 26, 2026

Commits on Sep 27, 2026

Commits on Sep 28, 2026

Commits on Sep 29, 2026

Commits on Sep 30, 2026

Commits on Oct 1, 2026

Commits on Oct 14, 2026

Commits on Oct 15, 2026

Commits on Oct 16, 2026

Commits on Oct 17, 2026

Commits on Oct 18, 2026