Daniel Dietsch
Daniel Dietsch
And I just realized #366 was with Integer memory model, not with Bitvectors.
Seems to be fixed with 70eefee1ca0ce7eb07006a5daa9aa48cc3087cbc @Jonas Can you confirm that ``examples\programs\acceleratedInterpolation\assertionError\oneLoopAssertionError.bpl`` is fixed and close the ticket?
For clarification: this issue is about predicate weakening.
@hauff What is missing for this?
Bug 2 also occurs in -tc AutomizerC.xml -s default/automizer/svcomp-Reach-32bit-Automizer_Default.epf -i examples/svcomp/loops/nec40.c and -i examples/svcomp/loops/n.c40.c
With the fix for bug 2 (6b6bf05) we get another issue: we have never tried to backtranslate ``((as const (Array Int Int)) 0)`` and hence get an exception in ``Term2Expression.translate(Term2Expression.java:238)``.
Cannot reproduce bug 1 on a5a1cc9f32 despite running for several hours. I checked past logs from struebli for occurrences and found only ``svcomp/pthread/queue_ok*`` examples with concurrency settings affected. The following...
d557452c96067381814099efdb22b1dbf299aa07 should fix bug 3.
Needs value completeness (see #438), because system with ``never a`` is fine
Older versions of this pattern required that the trigger part happens. E.g., https://ultimate-pa.github.io/hanfor/references/publications/formalization-analysis-rtrequirements.pdf 