diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs index 2e695215..19c88409 100644 --- a/Source/Provers/Z3/TypeDeclCollector.cs +++ b/Source/Provers/Z3/TypeDeclCollector.cs @@ -193,7 +193,12 @@ void ObjectInvariant() // there are a couple cases where operators have to be
// registered by generating appropriate Z3 statements
- if (node.Op is VCExprBvConcatOp) {
+ if (node.Op is VCExprBvOp) {
+ if (NativeBv) {
+ RegisterType(node[0].Type);
+ RegisterType(node.Type);
+ }
+ } else if (node.Op is VCExprBvConcatOp) {
//
if (NativeBv) {
RegisterType(node[0].Type);
|