Several fixes for SV-COMP

viktormalik commented 1 year ago

List of changes:

Support combination of --values-refine and --k-induction - so far, we supported --values-refine for AI only, which was fine since it was needed for heap for which we disabled k-induction. Now with the new unwinding, we need to support --values-refine for k-induction, too.
Disable --std-invariants for --k-induction as it causes more problems than just for the array invariants (fixed in #171). It also makes heap-data examples not to pass.
Make user inputs (from *scanf calls) non-deterministic.
Fixes for dynamic object splitting, array domain template, and witness generation

viktormalik commented 1 year ago

@peterschrammel do you think that disabling --std-invariants completely will cause some trouble?

viktormalik commented 1 year ago

Added some more fixes and updated the description. After this is merged, I'll do a new release.

viktormalik commented 1 year ago

cc @FrNecas

diffblue / 2ls