diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-07-09 12:38:12 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-07-09 12:38:12 -0700 |
| commit | b1b84b22d16894e5ea2bc7d677eb83c011cb6964 (patch) | |
| tree | 6fa7b6c9a35d63798dcb159810fc933bb065e39f | |
| parent | 574a0863cb34fb612ecf3d107416c955bdf889a8 (diff) | |
fixed bug in vcgen for bitvectors
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 7 | ||||
| -rw-r--r-- | Test/bitvectors/Answer | 3 | ||||
| -rw-r--r-- | Test/bitvectors/runtest.bat | 2 |
3 files changed, 10 insertions, 2 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);
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer index 6f4068c6..f0f65b04 100644 --- a/Test/bitvectors/Answer +++ b/Test/bitvectors/Answer @@ -49,6 +49,9 @@ Boogie program verifier finished with 0 verified, 1 error -------------------- bv8.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
+-------------------- bv10.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat index fd5136f5..a0480645 100644 --- a/Test/bitvectors/runtest.bat +++ b/Test/bitvectors/runtest.bat @@ -11,7 +11,7 @@ for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do ( echo -------------------- bv4.bpl - /bv:n --------------------
%BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl
-for %%f in (bv5.bpl bv6.bpl bv8.bpl) do (
+for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
|