Daniel Dietsch

**Describe the bug** After bare-metal install of paperless-ng, copy `media/` and `data/` from old paperless installation, ran `python manage.py migrate` followed by `python manage.py document_index reindex` without error. Then ran...

### Issue I am just setting up Tandoor with docker compose and an external reverse proxy in a subfolder. So far, I can access `https://domain/recipes/setup/`, but all requests to static...

Support GiB as unit

1

Currently, benchexec only accepts B, kB, MB, GB, and TB as units for memory limits. Because GiB is the usually used unit, it would be nice to also support it.

Bug: SMTLIBException: Timeout exceeded

1

SMTInterpol timeout is not converted to `TimeoutResult`. Instead, it is handled as an `ExceptionOrErrorResult`, thus canceling the whole verification. Stacktrace ``` de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Timeout exceeded at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:244) at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:226) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:876)...

### Basic Info * Version: 0.2.1-dev-bb7cadb (bb7cadb) * Settings: set ``--traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg=true`` ### Description Programs with non-deterministic calls like the following may trigger the exception below. We probably notice the bug...

IllegalArgumentException: unknown symbol (const Int (Array Int Int))

2

Version c3a52b3 File `loops/nec40.c` Severity: occurs on 11 of 2310 (https://struebli.informatik.uni-freiburg.de/logs/student-acceleration/20210416-091202-student-acceleration-259539aefe-M/overview) Stacktrace ``` java.lang.IllegalArgumentException: unknown symbol (const Int (Array Int Int)) at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:240) at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:129) at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:165) at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Term2Expression.translate(Term2Expression.java:129) at...

NegativeArraySizeException in DualJunctionTir$ExplicitLhsPolynomialRelations.buildDualFiniteJunction

1

Version c3a52b3 File `nla-digbench-scaling/hard-u_unwindbound5.c` Severity: occurs on 11 of 2310 (https://struebli.informatik.uni-freiburg.de/logs/student-acceleration/20210416-091202-student-acceleration-259539aefe-M/overview) Stacktrace ``` java.lang.NegativeArraySizeException: -1072721305 at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir$ExplicitLhsPolynomialRelations.buildDualFiniteJunction(DualJunctionTir.java:651) at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir$ExplicitLhsPolynomialRelations.buildCorrespondingFiniteJunctionForAntiDer(DualJunctionTir.java:615) at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir$ExplicitLhsPolynomialRelations.buildBoundConstraint(DualJunctionTir.java:451) at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryToEliminateConjuncts(DualJunctionTir.java:205) at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryToEliminateOne(DualJunctionTir.java:160) at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryExhaustivelyToEliminate(DualJunctionTir.java:125) at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.DualJunctionTir.tryToEliminate(DualJunctionTir.java:112) at...

AcceleratedInterpolation unsoundness ReachSafety-Loops

1

Version c3a52b33e1 There are numerous unsound results from AcceleratedInterpolation: https://struebli.informatik.uni-freiburg.de/logs/student-acceleration/20210416-091202-student-acceleration-259539aefe-M/results.2021-04-16_09-16-26.table.html#/table?filter=0(0*status*(category(in(wrong)))) The loop-zilu* examples produced accelerations with IcfgTransformation and had correct results (except one),the other ones did not produce accelerations with...

I would like to be able to use refinement strategies (e.g., WOLF,CAMEL) in conjunction with accelerated interpolation. I would also like AcceleratedInterpolation to detect situations in which it should accelerate...

We want to ensure that inputs are not constrained by requirements. We want to have separate environment assumptions. If inputs are constrained by requirements, we want to report the constraint...