summaryrefslogtreecommitdiff
path: root/Test/dafny4/Bug110.dfy.expect
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2015-12-02 12:35:54 -0800
committerGravatar qunyanm <unknown>2015-12-02 12:35:54 -0800
commitf7ab307779e4d21d706be13acad670d63d0e6537 (patch)
tree63ae17dcec2ebfdad7973af57799a5e00a2a85fc /Test/dafny4/Bug110.dfy.expect
parent223d3d98b80519f936cbdcc6ca31cdd2819bd900 (diff)
Fix issue 110. Set useImport to true when trying to registerTopLevelDecls
in MakeAbstractSignature.
Diffstat (limited to 'Test/dafny4/Bug110.dfy.expect')
-rw-r--r--Test/dafny4/Bug110.dfy.expect2
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/dafny4/Bug110.dfy.expect b/Test/dafny4/Bug110.dfy.expect
new file mode 100644
index 00000000..42fd56a5
--- /dev/null
+++ b/Test/dafny4/Bug110.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 8 verified, 0 errors