search

microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
223 stars 80 forks source link

l2s tactic crashes #75

Closed nano-o closed 4 years ago

nano-o commented 4 years ago

Hello, ivy_check crashes with a stack trace on the following, printing AttributeError: 'Sequence' object has no attribute 'labels'

#lang ivy1.7
include order
instance t : iterable
temporal property globally true
proof {
    tactic l2s
}
kenmcmil commented 4 years ago

Fixed in commit 27cfa56. Thanks.