summaryrefslogtreecommitdiff
path: root/Test/dafny4/set-compr.dfy.expect
blob: 615ee2bc49e155df35ead915a1975a23981b7fe1 (plain)
1
2
3
set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
set-compr.dfy(51,13): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
2 resolution/type errors detected in set-compr.dfy