Repository navigation

Add packaging mechanism to automatically build SV-Comp `zip` - #30

Draft

nils-loose wants to merge 373 commits into

mainfrom

dev

Draft

Add packaging mechanism to automatically build SV-Comp `zip`#30
nils-loose wants to merge 373 commits into
mainfrom
dev

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

Commits on Oct 16, 2026
- 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
- SV-COMP 2027 version (#92)
  nils-loose
  authored
  534c182
- Fix SV-COMP packaging of the single-file jar artifact; report the package version
  
  nils-loose
  and
  claude
  committed
  15ab838
- Merge pull request #94 from SWAT-project/fix/package-flat-artifact
  nils-loose
  authored
  2bd2bbf
- Embed bundled third-party component list in executor jar
  
  nils-loose
  and
  claude
  committed
  2ae41c2
- Add THIRD-PARTY-LICENSES.md generator for the SV-COMP package
  
  nils-loose
  and
  claude
  committed
  8764492
- Generate THIRD-PARTY-LICENSES.md when packaging, drop stale HTML report
  
  nils-loose
  and
  claude
  committed
  7f2a47d
- Merge pull request #95 from SWAT-project/chore/third-party-licenses
  nils-loose
  authored
  209cc0e
- Add optional executor phase profile (-Dswat.profile=<file>)
  
  nils-loose
  and
  claude
  committed
  0eb83cd
- Transformers return null for classes they do not change
  
  nils-loose
  and
  claude
  committed
  18800d8
- Send the trace with HttpURLConnection instead of HttpClient
  
  nils-loose
  and
  claude
  committed
  004231a
- Share the executor's classes across rounds with an AppCDS archive
  
  nils-loose
  and
  claude
  committed
  fdf08f0
- Profile: split premain into handler setup, thread context, input retrieval
  
  nils-loose
  and
  claude
  committed
  fe6fa18
- Run ASM's CheckClassAdapter only if instrumentation.checkClassAdapter is set
  
  nils-loose
  and
  claude
  committed
  a5997f2
Commits on Oct 21, 2026
- Solve floating-point queries with Z3's qffp tactic first
  
  nils-loose
  and
  claude
  committed
  1a67f8b
- Lift char codes as Java chars when the query only holds Java chars
  
  nils-loose
  and
  claude
  committed
  24219f2
- Merge perf/executor-round-cost into svcomp27/overnight-solver-perf
  
  nils-loose
  and
  claude
  committed
  c1f1456
- Merge perf/qffp-fp-tactic into svcomp27/overnight-solver-perf
  
  nils-loose
  and
  claude
  committed
  b845782
- Merge perf/char-code-bmp-lifting into svcomp27/overnight-solver-perf
  
  nils-loose
  and
  claude
  committed
  3f7e46f
Commits on Oct 27, 2026
- Update my-example-2
  solid-eureka
  committed
  f0745f9
- Lift chars widened to int in the int_to_bv lifting
  
  solid-eureka
  and
  claude
  committed
  b38d0ee
- Faster indexOf(int) encoding; keep surrogates in string literals
  
  solid-eureka
  and
  claude
  committed
  4fc51e1
- Use Z3 5.3.1 in the SV-COMP harness and the OpenOLAT target
  
  solid-eureka
  and
  claude
  committed
  23a4f62
- Solve int inputs that are only used as numbers over the Integers
  
  solid-eureka
  and
  claude
  committed
  d75d7a3
- Add --search-order: shallow, coverage and generational branch orders
  
  solid-eureka
  and
  claude
  committed
  177efe8
- Add --prefer-short-strings: shrink string inputs of a solution
  
  solid-eureka
  and
  claude
  committed
  19cd69a
- Run the property pre-check from cfg-extraction (#93)
  
  solid-eureka
  and
  claude
  committed
  28b8a38
- Ship the property pre-check jar in the SV-COMP archive (#93)
  
  solid-eureka
  and
  claude
  committed
  0313fca
- Cut the exception side of guards that cannot raise (#93)
  
  solid-eureka
  and
  claude
  committed
  90ca67a
- Prune by the graph under no-runtime-exception too (#93)
  
  solid-eureka
  and
  claude
  committed
  d2e0aa0
- Flag the branches of SWAT's helpers like callbacks
  
  solid-eureka
  and
  claude
  committed
  6344bd3
- Static pre-analysis for the HTTP driver
  
  solid-eureka
  and
  claude
  committed
  64c5174
- Raw request bodies in the HTTP driver; no halt on a diverged String
  
  solid-eureka
  and
  claude
  committed
  79322f9
- Report AssertionErrors where thrown for Spring endpoints
  
  solid-eureka
  and
  claude
  committed
  25419d3
- target-1: inserted bug in /e1/depth/5 for the SA experiments
  
  solid-eureka
  and
  claude
  committed
  7fea52e
- Keep null String and boxed endpoint parameters
  
  solid-eureka
  and
  claude
  committed
  15a42c6
- HTTP driver: sendable strings, and no hang when the driver fails
  
  solid-eureka
  and
  claude
  committed
  9911eb5
- personal-finance-engine-v2: switchable inserted bugs for the SA experiments
  
  solid-eureka
  and
  claude
  committed
  2461858
- HTTP mode: take static initializers out of the traces
  
  solid-eureka
  and
  claude
  committed
  db0b69b
- SA experiment campaign; switchable bugs in optaplanner-spring
  
  solid-eureka
  and
  claude
  committed
  61e8dfb
- Report the branches of inlined list lifting like a SWAT helper's
  
  solid-eureka
  and
  claude
  committed
  e9f0b88
- Campaign: bug-free case for the transaction filter endpoint
  
  solid-eureka
  and
  claude
  committed
  3287a51
- Results of the SA experiments on the applications
  
  solid-eureka
  and
  claude
  committed
  927ee10
- Note the work on relevance (slicing) and later loop summarization
  
  solid-eureka
  and
  claude
  committed
  db657fc
- swat-benchmarks: relevance and relevance-soundness suites
  
  solid-eureka
  and
  claude
  committed
  37cef25
- Relevance analysis: do not flip branches that cannot affect a target
  
  solid-eureka
  and
  claude
  committed
  4e884b1
- Relevance: a statement that may throw somewhere that matters is a branch
  
  solid-eureka
  and
  claude
  committed
  62ce5ae
- Slicing: solve the full query first, the sliced one where it has no model
  
  solid-eureka
  and
  claude
  committed
  3b8f4dc
- Document the relevance analysis: results, where it helps, design notes
  
  solid-eureka
  and
  claude
  committed
  8a1c51b
- Document the relevance limitations (library state, context) and their fixes
  
  solid-eureka
  and
  claude
  committed
  1f0166d
- swat-benchmarks: loop-summary and loop-summary-soundness suites
  
  solid-eureka
  and
  claude
  committed
  62b8c95
- Loop summaries: merge diamonds and counting loops into formulas
  
  solid-eureka
  and
  claude
  committed
  9a233cd
- Loop summaries: only merge values that stay symbolic
  
  solid-eureka
  and
  claude
  committed
  6283feb
- Document loop summarization: results, where it helps, the concretization bug, limits
  
  solid-eureka
  and
  claude
  committed
  8f86b67
- End deadlocked runs, and stop at a wall-clock deadline
  
  solid-eureka
  and
  claude
  committed
  bcac538
- Loop summaries for counting loops whose bodies do other things too
  
  solid-eureka
  and
  claude
  committed
  cb26a46
- Prefer small models over extreme ones
  
  solid-eureka
  and
  claude
  committed
  3c43ae7
- prefer_small: tolerate solutions of any shape
  
  solid-eureka
  and
  claude
  committed
  895deaa
- Loop summaries: nested conditions, division by constants, inclusive bounds
  
  solid-eureka
  and
  claude
  committed
  4dabcb6
- Document the loop summary next steps, small models and deadlocks
  
  solid-eureka
  and
  claude
  committed
  cc607da
- Explorer tests: driver fixtures for slicing and projected divergence
  
  solid-eureka
  and
  claude
  committed
  b319354
- Pin cfg-extraction v0.2.0 (data-flow facts for relevance)
  
  solid-eureka
  and
  claude
  committed
  71f1768
- CI: check out cfg-extraction without a token (#93)
  
  solid-eureka
  and
  claude
  committed
  0746098
Commits on Oct 28, 2026
- Bring swat-debug.cfg up-to-date with sv-comp.cfg
  solid-eureka
  committed
  1ada655
- Cleaner console log: explorer DEBUG only in the log files, no double prefix
  
  solid-eureka
  and
  claude
  committed
  359db51
- Log traces as DEBUG
  solid-eureka
  committed
  d38fe31
- Console log: executor lines with their own timestamp only; live output
  
  solid-eureka
  and
  claude
  committed
  41d70f2
- Log possible branch IDs as DEBUG
  solid-eureka
  committed
  27d7720
- Write the verdict to verdict.log
  
  solid-eureka
  and
  claude
  committed
  18de9b1
- Remove ThreadHandler's unused global Z3 context (fixes #110)
  
  solid-eureka
  and
  claude
  committed
  c17c0ef
- Remove ThreadHandler's unused global Z3 context (fixes #110)
  
  solid-eureka
  and
  claude
  committed
  2966bc3
- Remove ThreadHandler's unused global Z3 context (fixes #110)
  
  solid-eureka
  and
  claude
  committed
  52a8040
- Remove ThreadHandler's unused global Z3 context (fixes #110)
  
  solid-eureka
  and
  claude
  committed
  4e8d6b2
Commits on Nov 1, 2026
- Add comments
  solid-eureka
  committed
  6c4b590
- dfs: drop the UNMODELLED_EXCEPTION special-node case
  
  solid-eureka
  and
  claude
  committed
  3f2dfa4
- SA walk: one vocabulary, fewer special cases
  
  solid-eureka
  and
  claude
  committed
  d14b845
- dfs: one branch per role; test the walk counts; HTTP stats record them too
  
  solid-eureka
  and
  claude
  committed
  04a0ae5
- StrategyService logs to explorer.log; a shorter walk line
  
  solid-eureka
  and
  claude
  committed
  bcca759
Commits on Nov 2, 2026
- Type the SA code fully; it passes mypy
  
  solid-eureka
  and
  claude
  committed
  56fe56a
- Merge pull request #109 from SWAT-project/niklas/relevance-slicing
  solid-eureka
  authored
  66da216
- Merge svcomp27/overnight-solver-perf into dev
  solid-eureka
  committed
  f6c0d20
- Merge niklas/dev into dev
  
  solid-eureka
  and
  claude
  committed
  eb00840
Commits on Nov 3, 2026
- Make --search-order coverage the default
  
  solid-eureka
  and
  claude
  committed
  323f09e
- Merge niklas/coverage-default into dev: --search-order coverage by default
  
  solid-eureka
  and
  claude
  committed
  8c8394a
- SampledMath: sample the edges of the double and integral ranges
  
  solid-eureka
  and
  claude
  committed
  2a9ea29
- SV-COMP archive: ship and run the static pre-analysis
  
  solid-eureka
  and
  claude
  committed
  08e7a41
- cfg-extraction.ref: v0.2.1 (fat jar with component list, no GPL graph4j)
  
  solid-eureka
  and
  claude
  committed
  b24964c
- Merge niklas/svcomp-sa-package into dev: the SV-COMP archive runs the static pre-analysis
  
  solid-eureka
  and
  claude
  committed
  15759c0
- Loop-head states: Class.desiredAssertionStatus does not stop them
  
  solid-eureka
  and
  claude
  committed
  41f4072
- Prefer small models for floating-point inputs too
  
  solid-eureka
  and
  claude
  committed
  c8cdcc2
- Model floating-point % symbolically (it was silently concrete)
  
  solid-eureka
  and
  claude
  committed
  9eeba98
- Cap the resource limit of bounded re-solves
  
  solid-eureka
  and
  claude
  committed
  4caea36
- Size the limit of bounded re-solves by the branch's own query
  
  solid-eureka
  and
  claude
  committed
  2ff390a
- CLAUDE.md: small models for doubles, approximate models, loop-head state matching
  
  solid-eureka
  and
  claude
  committed
  5a0b895
Commits on Nov 4, 2026
- Merge dev into niklas/dev: the SV-COMP archive runs the static pre-analysis
  
  solid-eureka
  and
  claude
  committed
  8da25d3
- Merge niklas/dev into dev: approximate-model and loop-state fixes
  
  solid-eureka
  and
  claude
  committed
  64b9038

Commits

Commits on Oct 16, 2026

Commits on Oct 17, 2026

Commits on Oct 18, 2026

Commits on Oct 19, 2026