Closed panda2134 closed 1 month ago
Shown in the log as "'broadcast use' not implemented yet". Nevertheless, this should not crash Verus-analyzer over and over again and make it unusable.
Introduced by https://github.com/verus-lang/verus-analyzer/commit/21b57b346bf24a637b4cd09e278c39dcf5b943dd. It would be probably better to keep this commit away from the main branch anyway...
Closed via 4d9dba3
Shown in the log as "'broadcast use' not implemented yet". Nevertheless, this should not crash Verus-analyzer over and over again and make it unusable.