diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-23 12:07:20 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-23 12:07:20 -0800 |
| commit | c5c2c9465a53e4b35a20ad5efe73882dc6a5af34 (patch) | |
| tree | 9336173498839860956d21178bbf622d1bc22e77 /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | c7f74de7fae661883ca13bb09d557272de659e03 (diff) | |
removed call forall and * args to calls
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 3035c9de..d08a4d4b 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -647,12 +647,6 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false);
throw new cce.UnreachableException();
}
- public override Cmd VisitCallForallCmd(CallForallCmd node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
//Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<CmdSeq>() != null);
|