From 75cdf16714372ec03f1697450c135acdd3df9db3 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 29 Sep 2009 06:39:10 +0000
Subject: Fixed some bugs in the generation of bitvector input for Z3.
 Deleted/ignored some binaries in the Binaries directory.

---
 Source/Provers/Z3/TypeDeclCollector.ssc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/Provers')

diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc
index 86307b45..8173f7f3 100644
--- a/Source/Provers/Z3/TypeDeclCollector.ssc
+++ b/Source/Provers/Z3/TypeDeclCollector.ssc
@@ -117,7 +117,7 @@ namespace Microsoft.Boogie.Z3
       // there are a couple of cases where operators have to be
       // registered by generating appropriate Z3 statements
 
-      if (node.Op.Equals(VCExpressionGenerator.BvConcatOp)) {
+      if (node.Op is VCExprBvConcatOp) {
         //
         if (NativeBv) {
           RegisterType(node[0].Type);
-- 
cgit v1.2.3