Linard Arquint

Note that naively putting this Gobra-generated termination tuple element first instead of last does to work as demonstrated in the following example, as the (invisible) first tuple element increases from...

@jcp19 I ended up inlining some mutually recursive definitions where possible and in one case had to do the following: before: ``` ghost decreases getHeight(t) ensures ==> recursiveLabel(t, 0) ensures...

> Does this PR fix the version of silver and of the other submodules to the new release, or will we still get automated PRs every time the submodules are...

@jcp19 I've tried using the `ParallelTestExecution` trait that executes tests within a test suite in parallel on branch [`parallelize-GobraTests`](https://github.com/viperproject/gobra/tree/refs/heads/parallelize-GobraTests). While I can see an impressive speedup for just a few...

I thought this is a fairly recent regression but I can't find the commit on which it worked: - Reproducible on latest `master` commit: ac4a94b21f2f3e55bd8c7299ae9fbc422e999d41 - Reproducible on latest `hyperGobra`...

`v1` works flawlessly but when changing the tag to `v2`, the error mentioned above occurs

Thanks for the pointer! I think that's exactly the problem. I've observed the issue in a PR created by Dependabot and I guess the corresponding CI run (on push) does...

@karalarmehmet Hi Mehmet! I did not spend too much time on this issue as this action became no longer necessary for our use case at pretty much the same time...

another one: ``` package foo func floatfn3(f float64) float64 { return 0.0 } ``` It seems to me that a float literal causes the issue (probably in the type checker)

Regression (just in case we are not aware of it yet): in contrast to 8facab51220570ff88f72e71e794bcb336208e47, termination measures are no longer transformed resulting in crashes of Silicon