Add packaging mechanism to automatically build SV-Comp `zip` by nils-loose · Pull Request #30 · SWAT-project/SWAT

nils-loose · 2026-06-24T12:57:21Z

No description provided.

nils-loose · 2026-06-29T14:12:11Z

+  SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content
+  SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6


@k0lja Can you propose a different mechanism, perhaps another repository here that publishes the required files, I dont want to reference zenodo here in the CI

In addition, the venv we are using is built on the specific ubuntu version required by sv-comp. updating the dependencies is a hassle atm. Can you check if it could be possible either here or in the supporting repo (for the above) you can actually build the venv based on the requirements (pip freeze the current venv) as part of the ci there? this would make updating the venv much easier

nils-loose · 2026-06-29T14:15:48Z

+    - name: Build WitnessCreator JAR
+      run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar


As discussed could you also move the full witness creator into its own repo that publishes an artifact we can use here?

nils-loose · 2026-06-29T14:17:07Z

@@ -18,8 +23,142 @@ jobs:
        distribution: 'temurin'
    - name: Setup Gradle
      uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4


While you are at it, could you also check why the setup-gradle v4 is referenced using this hash I assume? is that the proper way to do that? (I know this is older then your changes but I was wondering for some time)

nils-loose · 2026-06-29T14:17:49Z

This entire package of supporting file should then also move into the supporting repo I guess?

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Two branches of one trace can share an iid (switch case index wraps at 16, loop counter at 64), and one got the other's constraint: false SAFE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…inside) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…omp27/integration

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…call tree The graph's only targets are assert sites, so pruning by it under any other property (no-runtime-exception) drops paths to the violation. The explorer now runs no pre-analysis unless the property is valid-assert, and logs why; the harness no longer passes --sa-path for other properties. The walk follows main's call tree only, so an assert run by a shutdown hook, another thread or an uncaught-exception handler is on no path it knows. A graph with a library call that hands application code to such an entry (Thread.start, addShutdownHook, set*UncaughtExceptionHandler, executor submission, Timer, *Async) is not used. When a callback reaches an assert, leaving main normally or by an exception is interesting too, since such a callback may still run after main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

When the trace's branch key or a frame of its call stack is missing, check_branch cannot tell whether the walk is still in step. The walk still follows the graph there, so later branches can be checked, but no side of that branch is pruned. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

DfsTest trees now carry branch keys and stack deltas, since unkeyed pairings no longer prune. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

FCMP built its formula from greaterThan and FP equality only, so a NaN operand compared as 'less' in the formula, while the JVM pushes 1 (FCMPG) or -1 (FCMPL). The solver could then pick NaN to satisfy an ordered comparison such as 0.0f <= x, and the run took the other side. The concrete value used Float.compareTo, which orders -0.0f below 0.0f and NaN above everything. Mirror DoubleValue.DCMP: an explicit NaN case in the formula and IEEE comparisons for the concrete value. A concrete NaN operand no longer drops the formula. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The nondet redirect assumed a ()X descriptor and produced an invalid descriptor for nondetObject(Class, ObjectFactory), so instrumenting the calling class failed. nondetObject is defined as factory.createObject(), and the factory makes its choices with the primitive nondet methods, so the call is now rewritten to the factory call in the instrumented caller: the factory's nondet values are symbolic and every object it can return is explored. A factory that is not instrumented makes concrete choices; its createObject call is recorded as a context loss so that SAFE is downgraded. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

A run that does not take the side its solution was solved for used to leave the branch solved, so its unexplored side was never tried again and SAFE was ruled out (unexpected_divergence). Most such runs end in an OutOfMemoryError before the branch: Z3 picks a size such as 2^31-1 and the allocation fails, though small sizes reach the branch. Now the branch becomes a candidate again, up to --divergence-retries times (default 3). A retry excludes every solution that failed so far and looks for small values first: integral inputs bounded by 16, 256 and 65536 in turn, then unbounded. UNSAT under these extra constraints proves nothing, so it is never recorded as an infeasible branch. Only when all retries diverge, or no other solution is left, is the branch given up on and recorded as unexpected_divergence (or as an expected divergence for an approximate model, as before). A given-up branch rules out SAFE unless another run reached its unexplored side by the end of the search. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

… be added Every Database method now holds the lock in a with-block. An exception in add_trace (a RecursionError on a long trace) used to leave it held, and the driver then waited for it until the time limit. get_violations also returned with the lock held for an unknown endpoint. add_trace records the soundness flags before it adds the trace to the tree, so they hold even if that fails. ConstraintService catches a failure, logs it and records a trace_ingest_failed execution error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

- An exception in the exploration ends the run at once with UNKNOWN and an explorer_crash execution error. Before, the worker thread died, the HTTP server kept the process alive and the run hung until the time limit. run_sv_comp prints DONT-KNOW for anything that fails around the driver and exits. - A trace that could not be added ends the search with UNKNOWN: the tree lacks its path. A violation in the same run still counts. - The divergence check only runs when the round sent a trace. Before, it checked the previous round's trace. A round without a trace records no_trace: its branch counts as solved and is never tried again. - tree_mismatch, trace_ingest_failed, no_trace and explorer_crash rule out SAFE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The walk was recursive and visited shared subterms once per path to them, which is exponential in the depth of a DAG. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

- The explorer logs relayed executor output (log.RELAYED) as it is, without its own timestamp, thread and level in front of the executor's. - The harness reads a task's output while it runs and, in single mode, prints each line when it arrives instead of all of them at the end. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

get_verdict_logger() returned the explorer logger, so verdict.log stayed empty. The verdict still goes to explorer.log too, and is printed once on the console. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ThreadHandler.init() created a Z3 SolverContext that nothing ever read, and never closed the previous one. Six test classes called it before every test case, so each case leaked a whole Z3 context (about 17 MB): the executor tests peaked above 22 GB, and GitHub's runner (16 GB) was shut down in the middle of :symbolic-executor:test. Without it the tests peak at 1.9 GB, and the executor no longer creates an unused Z3 context at the start of every run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ThreadHandler.init() created a Z3 SolverContext that nothing ever read, and never closed the previous one. Six test classes called it before every test case, so each case leaked a whole Z3 context (about 17 MB): the executor tests peaked above 22 GB, and GitHub's runner (16 GB) was shut down in the middle of :symbolic-executor:test. Without it the tests peak at 1.9 GB, and the executor no longer creates an unused Z3 context at the start of every run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit c17c0ef)

Since 373384d the marker is no tree level: Tree.structural keeps it as the unmodelled_exception flag on the node after it, and Tree.add is the only place that builds nodes. The walk's check for a marker node could only be reached by hand-built trees in test_sa_walk, which now set the flag instead. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

dfs (strategy/DFS.py) now reads as its three steps per branch: pair it with the graph (_pair), prune, slice (_classify). How a branch was paired is one of verified, resynced, unverified, lost or masked, and the walk counts those (Tree.walk) and logs one line per selection ("[DFS] Walk: ..."), also written to stats.json (static_analysis.last_walk). The walk state is a named tuple instead of an 8-tuple; dfs loses the parameters only it used itself (visited, clinit_depth, sa_stack, sa_index, trace_stack). Merged and sliced branches are one classification. SAGraph: target points are SANode.isTarget, reachesTargetSameLevel and targetDistance (no longer named after asserts). Dropped what nothing needs any more: graphs without return sites (and their context-insensitive marking), isPhantomGuard, the RETURN edge lists, the child accessors, and the call site's fall-through to its one callee. SANode.handler_for replaces three copies of the handler lookup. Relevance: the unused constructor parameter is gone, the closure of methods running a relevant branch is computed by one helper. Node and Leaf have class defaults for every per-node flag, so neither the walk nor tests need getattr fallbacks. Removed --sa-retry-without (explorer and harness): a guard against false SAFE from SA bugs from before keys checked the walk; desyncs now turn SAFE into UNKNOWN instead. The analysis results are unchanged: every node's summaries, relevance, regions and distances are the same as before on all 2201 graphs of sv-benchmarks and swat-benchmarks (valid-assert and no-runtime-exception). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…m too Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

StrategyService used a module logger, which reaches neither explorer.log nor the console: its walk summary (and, before, the relevance and loop-state lines) were never seen. It now uses the explorer's logger; is_symbolic_branch's two INFO lines per new candidate are one DEBUG line. The walk line uses the documented terms: [DFS] Walk: 34 branches (33 verified, 0 resynced, 0 unverified, 0 lost, 1 masked), 12 sides pruned; 32 sliced, 0 merged, 0 covered, 0 poisoned Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The SA modules (DFS, StrategyService, SAGraph, Relevance, the tree classes, StaticPreAnalysis) pass mypy with --check-untyped-defs --disallow-untyped-defs --disallow-any-generics. Named types instead of bare tuple/dict/set: - SAGraph: Location and Effect (the data-flow facts: dataflow is tuple[Effect, ...], control tuple[Location, ...]), CallFacts (a TypedDict for the `call` field), ExceptionChain, TraceFrames and TraceStack. LOST is an enum sentinel, so `is LOST` narrows. - Relevance: CfgNode (a graph node or a virtual EXIT/EXIT_EXC/END), Method (str | None: nodes without method metadata). - DFS: Pairing and Role are Literal types, OpenRegions names the region list; dfs's walk state is fully typed. - Node: Ident and BranchName (a candidate's identity); Branch: Position and PositionedState (loop-head states). - StrategyService.select_branch takes named parameters instead of **kwargs; `-> list()` return annotations (a call, not a type) are list[str]. Where a value is Optional in general but always set where it is read, there is now one accessor with an assertion instead of an unchecked read: SANode.sides() (a branch's two successors) and resume_site() (a call site's return site). dfs keeps the verified graph node in one variable (None unless the pairing was verified), which is what the pruning and slicing checks. Also: the Leaf docstring is its __doc__ again, Node caches its depth in a declared field (depth_cache) instead of a getattr'd _depth, and loop variables that were reused with another type in Relevance are renamed. Every node's analysis results are unchanged on the 2201 graphs from sv-benchmarks and swat-benchmarks; all explorer tests pass. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Relevance (slicing) and loop summaries; rebased onto svcomp27/overnight-solver-perf

Brings in the overnight solver performance work (#96, #98, #99), the property pre-check in cfg-extraction (#108), and relevance slicing and loop summaries (#109). The one conflict, in Transformer.java, comes from the #110 fix having been committed on both branches; resolved as on the overnight branch. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> # Conflicts: # symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java

Brings in the SA cleanup (one vocabulary for the walk, legacy graph format and --sa-retry-without removed, walk counts in the log and in stats.json), full type annotations of the SA code, and the console log changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Against dfs (300 s, with SA, 2026-11-03), coverage found 6 more violations on swat-benchmarks and 4 more on sv-benchmarks valid-assert that dfs did not find in five runs, lost only a flaky one, and left every SAFE verdict as it was. On no-runtime-exception it missed one real bug dfs finds (WeibullGenerator_exceptionless, whose label is wrong and is fixed locally in the sv-benchmarks checkout). The harness now always passes --search-order, so that an explicit --search-order dfs is not lost to the explorer's default. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…fault Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The approximate Math models were exact only at "nice" inputs (small numbers, multiples of pi) and at inputs giving nice outputs, so a result that overflows to infinity or becomes NaN could not be reached: Math.pow(0.69, (int) (1 / beta)) is +Infinity only for an exponent of about -1940 or less, which is no sample. sv-benchmarks WeibullGenerator_exceptionless throws for such a beta, and its throw branch was UNSAT, or out of the resource limit, in every round; dfs found the bug only through a lucky model of another branch, coverage not at all. The tables now also sample Integer and Long MIN/MAX_VALUE, +-Double.MAX_VALUE, +-Double.MIN_VALUE, +-Infinity and NaN. The task's throw branch is then solved directly: VIOLATION in 11 rounds with coverage, 16 with dfs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The archive only shipped the property pre-check, and run_swat.py passed no --sa-path, so SA never ran there. Now: - CI builds cfg-extraction's fatJar next to precheckJar, and package-svcomp.sh ships it as cfg-extraction/cfg-extractor.jar. - The explorer takes the extractor jar itself with --sa-jar (--sa-path still takes a checkout). - run_swat.py passes --sa-jar under valid-assert only (as the harness does) and --target Main. Without --target the graph's entry was None and the extractor failed, silently leaving the run unpruned; StaticPreAnalysis now also defaults the entry to Main, the class the executor runs. - third_party_licenses.py lists the fat jar's components (needs its META-INF/swat-third-party.json from cfg-extraction's fatJarComponentList) and maps SootUp's and JGraphT's license names. - check-svcomp-package.sh fails unless the smoke test's static pre-analysis loaded its graph. Needs a cfg-extraction release with fatJarComponentList in cfg-extraction.ref (v0.2.0 has none). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

… static pre-analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Since ca0f2a5 a run reports no more loop-head states after a call into untracked code other than a few pure methods. The static initializer of every class with an assert calls Class.desiredAssertionStatus (javac's $assertionsDisabled), so every valid-assert task stopped reporting before main started, and loop-state matching pruned nothing in any task of sv-benchmarks or swat-benchmarks (2026-11-03). desiredAssertionStatus reads the JVM's assertion setting, which is the same in every run, and its result lands in a static field of the application class, which is hashed. float_unboundedloop/ Batch-Conveyor-Counter, whose state cycles, is SAFE again in 4 rounds (UNKNOWN at the timeout without states). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

With the extreme samples of the Math models (2a9ea29), Z3 started to pick huge doubles (2^67 and beyond) for coral45 and coral53: there the model of exp() is the value of the previous run, not the real one, so every such solution diverged, and after the retries the branch was given up (UNKNOWN in 17 s; both were found in every run before). A solution with a floating-point input beyond 65536 in magnitude, or an infinite one, is now re-solved with the inputs bounded first, as for integral inputs, and the divergence retries bound floating-point inputs too (excluding NaN and infinities in the bounded tries; the unbounded try comes last). coral45 and coral53 are found again, and EquidistantConicProjection_true, whose violation needs infinite inputs, still is (its label is wrong, fixed locally). The bounds are built in the value's own context: z3.fpGEQ, z3.fpAbs and unary minus use the global one, which crashed or failed with the solver's shared context. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

DREM and FREM returned the concrete remainder without a formula and without a soundness flag, so every branch on a remainder looked concrete: a search that never ran into the violation by chance reported SAFE. With the floating-point small-model preference (c8cdcc2) the early runs of sv-benchmarks PieSegment_false/_true took other inputs, and both came out SAFE although both violate valid-assert (angle % 360 is negative for a negative angle). The remainder is now a model like the transcendental Math functions (SampledMath#define, now public and typed by its arguments): exact where the quotient is at most 1 in magnitude (x for |x| < |y|; |x| - |y| with x's sign for |y| <= |x| < 2|y|, exact by Sterbenz), the concrete result elsewhere, and declared approximate, so a branch on it is a precision loss. PieSegment_false and _true are VIOLATION again, in 4 rounds. The exact encoding (fp.rem, adjusted by one |y| where its sign differs from x's) is correct but too slow: Z3 did not decide angle % 360 < -180 for a symbolic double within 120 s; the model takes milliseconds. JavaRemainderSpec checks the model against Java's % bit for bit on edge values of doubles and floats. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The small-model preference and the bounded divergence retries only look for a nicer solution, but ran without a resource limit. Bounding floating-point inputs (c8cdcc2) can make a query far harder: ReverseInterpolator_false and _false2 spent 261 s on one bounded query, until the CPU deadline, instead of running the original solution, which reaches the violation. Each bounded query now gets at most 10M resource units (about 4 s, BOUNDED_RLIMIT); running out moves on to the next bound or keeps the original solution. Both tasks are VIOLATION again in 3 rounds; coral45 and coral53 stay found. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The fixed 10M-unit cap (4caea36) was too small where the query is expensive anyway: jbmc-regression/calc needs 22M units unbounded and 25M bounded; capped, the bounded query ran out, the run took the original solution with an array size of 2^31 - 1 and ran out of memory (SAFE -> UNKNOWN), and coral61/coral62 lost their violations the same way. The limit is now twice what the branch's unbounded query used, at least 10M (Z3Handler.last_rlimit_used, recorded per branch). calc is SAFE again, coral61/62 and ReverseInterpolator_false are VIOLATION. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…ate matching Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…alysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Extreme samples for the Math models, floating-point % as an approximate model (it was silently concrete: false SAFE), small models for floating-point inputs with bounded re-solves capped, and loop-head state matching working again for programs with asserts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

nils-loose commented Jun 29, 2026

View reviewed changes

solid-eureka and others added 29 commits October 16, 2026 20:21

SA walk: resume at the handler after an unmodelled exception

50ce3ff

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: handler resumption tasks

7f6aa4c

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Docs: handler resumption results

b3a08e7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Executor: report branch keys and stack changes in the trace

1568fec

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SA walk: detect desyncs by key and resync after losing the graph

fc817ee

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Docs: branch keys, desync detection and resync

66a5d02

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Remove handler resumption (covered by resync)

8f5505e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Mask library callbacks in the SA walk

aa20dab

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: library callback tasks; docs

8dab346

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: library-callback-assert (known false SAFE with SA)

d8289a7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Flag to turn off callback targets (--sa-no-callback-targets)

6ced24e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Key the solver's constraint cache by tree node, not iid

f6197d3

Two branches of one trace can share an iid (switch case index wraps at 16, loop counter at 64), and one got the other's constraint: false SAFE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: exec-loop-iid-wrap

9046cd0

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Keep Z3's jar off the extractor's classpath

69c6b83

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SA walk: call sites with several callees (union in summaries, resync …

98eb95d

…inside) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Docs: callback targets, multi-target calls, solver cache fix

65aab6e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Remove dead code left from the SA integration

604ba0a

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Remove generated timing plot, ignore it

8f0501b

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge remote-tracking branch 'origin/feat/witness-via-trace' into svc…

2f8e874

…omp27/integration

Merge #65 (static pre-analysis) into the integration branch

e65dbe2

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Tests for the pre-analysis guards and unchecked pairings

aa8a0ef

DfsTest trees now carry branch keys and stack deltas, since unkeyed pairings no longer prune. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Extract constraint variables without recursion, each subterm once

58c15ae

The walk was recursive and visited shared subterms once per path to them, which is exponential in the depth of a DAG. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

solid-eureka and others added 30 commits October 28, 2026 11:12

Log possible branch IDs as DEBUG

27d7720

Write the verdict to verdict.log

18de9b1

get_verdict_logger() returned the explorer logger, so verdict.log stayed empty. The verdict still goes to explorer.log too, and is printed once on the console. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Add comments

6c4b590

dfs: one branch per role; test the walk counts; HTTP stats record the…

04a0ae5

…m too Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge pull request #109 from SWAT-project/niklas/relevance-slicing

66da216

Relevance (slicing) and loop summaries; rebased onto svcomp27/overnight-solver-perf

Merge niklas/coverage-default into dev: --search-order coverage by de…

8c8394a

…fault Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

cfg-extraction.ref: v0.2.1 (fat jar with component list, no GPL graph4j)

b24964c

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge niklas/svcomp-sa-package into dev: the SV-COMP archive runs the…

15759c0

… static pre-analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

CLAUDE.md: small models for doubles, approximate models, loop-head st…

5a0b895

…ate matching Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge dev into niklas/dev: the SV-COMP archive runs the static pre-an…

8da25d3

…alysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Navigation Menu

Repository navigation

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

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

nils-loose commented Jun 24, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content
		SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6

		- name: Build WitnessCreator JAR
		run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar

Conversation

nils-loose commented Jun 24, 2026

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants