summaryrefslogtreecommitdiff
path: root/Source/Dafny/Printer.cs
diff options
context:
space:
mode:
authorGravatar Jason Koenig <unknown>2012-06-13 19:02:21 -0700
committerGravatar Jason Koenig <unknown>2012-06-13 19:02:21 -0700
commit998d686fdb6b31d25ef2b9f995f64a0187a154c9 (patch)
tree44097d73b01d71f16e2174c4c7fc0c52adf34fd9 /Source/Dafny/Printer.cs
parent84219c03a73e14a7b0a74c4e94b38b8855f13fa7 (diff)
parentde2e6cad0c25388aca044d42ad3cbd1a873f7637 (diff)
Merge
Diffstat (limited to 'Source/Dafny/Printer.cs')
-rw-r--r--Source/Dafny/Printer.cs5
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index e58a39de..fb46ba4b 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -661,7 +661,10 @@ namespace Microsoft.Dafny {
} else if (s is AssignSuchThatStmt) {
var update = (AssignSuchThatStmt)s;
wr.Write(" :| ");
- PrintExpression(update.Assume.Expr);
+ if (update.AssumeToken != null) {
+ wr.Write("assume ");
+ }
+ PrintExpression(update.Expr);
} else {
Contract.Assert(s == null); // otherwise, unknown type
}