Daniel Dietsch

@tautschnig Mainly because we currently do not support ``abort()`` but ``VERIFIER_assume()``, we do not have to think about it just yet. We model ``__VERIFIER_assume()`` as ``assume``, i.e., if the assume...

@mdangl @tautschnig I totally agree with Matthias and I think we labeled all the tasks according to the understanding that an assume does not cause non-termination. I am not sure...

@tautschnig : Exactly! Its neither terminating nor non-terminating because there is no program execution.

``printf`` should be fixed by 05c55e3, ``sprintf`` can be fixed either with full support or just as uninterpreted function (@alexandernutz , thoughts?), and ``fprintf`` will not be supported for quite...

So you saying with the changed flag it works for you? Note: we still have to fix ``sprintf`` and ``fprintf``

70eefee1ca0ce7eb07006a5daa9aa48cc3087cbc fixed the loop-zilu* examples (see https://struebli.informatik.uni-freiburg.de/logs/index.php?dir=student-acceleration/20210501-092903-student-acceleration-1a84f7301f), but two examples still remain unsound: https://struebli.informatik.uni-freiburg.de/logs/student-acceleration/20210501-092903-student-acceleration-1a84f7301f/results.2021-05-01_09-28-41.table.html#/table?filter=2(0*status*(category(in(wrong)))) @JonasWerner can you investigate?

So far I was unable to reduce the example in a meaningful way. It might be that the syntax errors of the original file are now catching up to us.

@Heizmann thank you. I added the example in 5c05803

We should keep this open for now.

New actual: Actual: rt-inconsistent:req1+req2; vacuous:req1; inconsistent:; The vacuous part is still an issue.