MartinSpiessl
MartinSpiessl
The previous wording could be read such that the cache is cleared in the background once the expiration time is reached. However this is not the case, so we simply...
Last year we had some problems with the score calculation because a validator falsely flagged witnesses as invalid. As a result, the code that prevents a witness from counting as...
This task contains an overflow, so stating the termination property makes no sense, especially since no verdict is given.
As described by me in https://github.com/sosy-lab/sv-benchmarks/pull/920#issuecomment-675283861 > I see some problems with this PR: > > 1. The corrected version of the program just sets the divisor to 1 instead...
For the proposed category, it is still unclear how the witnesses would/should look like and whether we will have any validators for this.
I would really welcome if this procedure were documented somewhere. I know that we say that a PR can be merge if it has at least one approving review. I...
The programs freire{1,2}.c in `c/nla-digbench` are clearly flawed since they neglect the limited floating point precision. As an example, let's look at this concretized version of `freire1.c`: ``` #include #include...
Please add other open points about the category structure for this year's SV-COMP to this issue once they surface. - Juliet Tasks: From last year (https://github.com/sosy-lab/sv-benchmarks/issues/819) we still have to...
*This is part 2 of two closely related issues, the first one (#1123) building the base for implementing this one.* We could try to allow for unpreprocessed program files to...
*This is part 1 of two closely related issues, the second one (#1124) building upon this one.* It has become more and more labor-intensive over the past years to maintain...