Nontermination bug with nested match patterns

[tinelli]

Nested patterns in match make lfscc diverge. See example.

(declare A type)

(declare list type)
(declare nil list)
(declare cons (! a A (! l list list)))

(program p ((a A) (l list)) A
  (match l 
    (nil a)
    ((cons a1 nil) a1)
    ((cons a1 (cons a2 nil)) a1))
)