diff options
| author |  qunyanm <unknown> | 2015-03-31 09:17:26 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-03-31 09:17:26 -0700 |
| commit | b4b193a05571b243d50a832dae58e837e779b710 (patch) | |
| tree | e4c2f9707ee8c9bcb449a5e61b9d89be6f1cb7bc /Test/dafny4/set-compr.dfy.expect | |
| parent | 441eca2a4c02efcc555cb8ca25ac991ccee205f8 (diff) | |
Fix issue 61. Decreases are by default in ghost context. Therefore,
dontCareAboutCompilation flag should be set to false in the ResolveOpts.
Diffstat (limited to 'Test/dafny4/set-compr.dfy.expect')
| -rw-r--r-- | Test/dafny4/set-compr.dfy.expect | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect new file mode 100644 index 00000000..b31c6ac0 --- /dev/null +++ b/Test/dafny4/set-compr.dfy.expect @@ -0,0 +1,3 @@ +set-compr.dfy(25,7): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+set-compr.dfy(51,13): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+2 resolution/type errors detected in set-compr.dfy
|