viperproject
Sequence-related incompletenesses
Created by @alexanderjsummers on 2019-05-16 13:36 Last updated on 2019-05-16 13:37
This is a catch-all issue for observable incompletenesses in the sequence axiomatisation. Since I started upgrading the version that Carbon uses (and we haven’t yet unified the input definitions for the two tools), some incompletenesses in Silicon are no-longer incompletenesses in Carbon. However, since Silicon’s axiomatisation also contains some axioms (e.g. from Dafny) which are not used in Carbon, the reverse can also be true.
@alexanderjsummers commented on 2019-05-16 13:37
See also https://github.com/viperproject/silicon/issues/380
and
https://github.com/viperproject/silver/issues/80