Wrong solutions for combination of blackhole and non-determinism
Consider the following program:
main = let x = True ? fcase x of True -> False in x
With respect to the corrected natural semantics of FlatCurry, this defition has only one value: True. However, PAKCS computes both True and False as solutions before it enters an infinite loop:
blackhole> main
True
False
Prolog interruption (h for help)?
In contrast, the KiCS2 computes only the single value True before it enters the infinite loop.