Fix issue 128. Change the translation of CanCallAssumption for let-such-that

expression from
      // CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] =
      //   (forall b0,b1 :: typeAntecedent ==>
      //       CanCall[[ RHS(b,g) ]] &&
      //       (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) &&
      //       $let$canCall(b,g))
to
      // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] =
      //   $let$canCall(g) &&
      //   CanCall[[ Body($let$b0(g), $let$b1(g), h) ]]

1 files changed, 5 insertions, 3 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index accdb9d3..86c493f1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1955,9 +1955,11 @@ namespace Microsoft.Dafny {
         var e = (BoxingCastExpr)expr;

         PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, keyword);
       } else if (expr is Translator.BoogieWrapper) {
-        wr.Write("[BoogieWrapper]");  // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here
-      } else {
-        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
+        wr.Write("[BoogieWrapper]");  // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here

+      } else if (expr is Translator.BoogieFunctionCall) {

+        wr.Write("[BoogieFunctionCall]");  // this prevents debugger watch window crash

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }
     }