diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-22 13:39:02 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-22 13:39:02 -0800 |
| commit | a587a83b6e78bcfe2f74173f0d9a4d3aeb54c6e3 (patch) | |
| tree | 91cbb75455bb31513edb1a9ed437eb65c1c649b7 /Source/Houdini/Houdini.cs | |
| parent | b4634db9bc0f3457752dcee52176dcc87c0157a9 (diff) | |
bug fix in the FreeRequiresVisitor
Diffstat (limited to 'Source/Houdini/Houdini.cs')
| -rw-r--r-- | Source/Houdini/Houdini.cs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 0b331356..2ed147d1 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -288,6 +288,14 @@ namespace Microsoft.Boogie.Houdini { else
return new Requires(true, requires.Condition);
}
+
+ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ node.Requires = base.VisitRequires(node.Requires);
+ node.Expr = this.VisitExpr(node.Expr);
+ return node;
+ }
}
public class Houdini : ObservableHoudini {
|