From 241de8264a32285d371a53d8d91a219625d76922 Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Mon, 7 Mar 2011 05:15:14 +0000
Subject: Fix contracts so runtime checking can be turned on.

---
 Source/VCExpr/SimplifyLikeLineariser.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/VCExpr/SimplifyLikeLineariser.cs')

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 45eeda43..c907bd9f 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -335,14 +335,14 @@ namespace Microsoft.Boogie.VCExprAST {
 
     public static string StoreOpName(VCExprNAry node) {
       Contract.Requires(node != null);
-      Contract.Requires((node.Op is VCExprStoreOp));
+      Contract.Requires((node.Op is VCExprSelectOp) || (node.Op is VCExprStoreOp));
       Contract.Ensures(Contract.Result<string>() != null);
       return "Store_" + TypeToString(node[0].Type);
     }
 
     public static string SelectOpName(VCExprNAry node) {
       Contract.Requires(node != null);
-      Contract.Requires((node.Op is VCExprSelectOp));
+      Contract.Requires((node.Op is VCExprSelectOp) || (node.Op is VCExprStoreOp));
       Contract.Ensures(Contract.Result<string>() != null);
       return "Select_" + TypeToString(node[0].Type);
     }
-- 
cgit v1.2.3