You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
On the following example, Zipperposition does not respect the --timeout 2 option but fills all the available memory:
data list a := nil | cons a (list a).
def[infix "++"] append : pi a. list a -> list a -> list a where
forall l. append nil l = l;
forall hd tl l. append (cons hd tl) l = cons hd (append tl l).
def foreach : pi a. list a -> (a -> prop) -> prop where
forall p. foreach nil p = true;
forall hd tl p. foreach (cons hd tl) p = (p hd && foreach tl p).
goal forall a (l1 l2 : list a) p. foreach (append l1 l2) p = (foreach l1 p && foreach l2 p).
Called with zipperposition --timeout 2 bug.zf.
The text was updated successfully, but these errors were encountered:
rafoo
pushed a commit
to rafoo/zipperposition
that referenced
this issue
Jun 3, 2017
On the following example, Zipperposition does not respect the
--timeout 2
option but fills all the available memory:Called with
zipperposition --timeout 2 bug.zf
.The text was updated successfully, but these errors were encountered: