Symbolic Execution not terminating

[weaversa]

parity xs = ys!0
  where ys = [False] # [y ^ x | x <- xs | y <- ys ]

prefix f xs = ys!0
  where ys = [xs@0] # [ f y x | y <- ys | x <- tail xs ]

par = prefix (^)

Main> :prove \(x:[2]) -> (par x) == (parity x)
Using exhaustive testing.
passed 1024 tests.
QED
Main> :prove \(x:[1]) -> (par x) == (parity x)

Another example (much simpler than Mark's) where the symbolic execution is not terminating, but should.

[brianhuffman]

Fixed in 337b7d3. It was an issue with the symbolic simulator being too strict in the presence of recursive definitions. I'll close the issue as soon as I get around to adding a regression test for this.