diff options
| author |  rustanleino <unknown> | 2009-09-29 06:39:10 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-09-29 06:39:10 +0000 |
| commit | 75cdf16714372ec03f1697450c135acdd3df9db3 (patch) | |
| tree | c218a23b5f4030241dd419d170d274d7e26399c7 /Source/Provers/Z3 | |
| parent | 84121f913cd1e4f78847bb246c2a83ac116a1a1b (diff) | |
Fixed some bugs in the generation of bitvector input for Z3.
Deleted/ignored some binaries in the Binaries directory.
Diffstat (limited to 'Source/Provers/Z3')
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.ssc | 2 |
1 files changed, 1 insertions, 1 deletions
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);
|