diff options
-rw-r--r-- | Source/Core/AbsyCmd.cs | 4 | ||||
-rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 7 | ||||
-rw-r--r-- | Test/bitvectors/Answer | 3 | ||||
-rw-r--r-- | Test/bitvectors/bv10.bpl | 10 | ||||
-rw-r--r-- | Test/bitvectors/runtest.bat | 2 |
5 files changed, 22 insertions, 4 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 825efa21..def13f7d 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1915,8 +1915,8 @@ namespace Microsoft.Boogie { if (QKeyValue.FindBoolAttribute(this.Attributes, "async") && Outs.Count > 0) {
Type returnType = cce.NonNull(Outs[0]).ShallowType;
- if (!returnType.Equals(Type.Int)) {
- tc.Error(this.tok, "the return from an asynchronous call should be an integer");
+ if (!returnType.Equals(Type.Int) && !returnType.Equals(Type.GetBvType(32))) {
+ tc.Error(this.tok, "the return from an asynchronous call should be either int or bv32");
return;
}
}
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/bv10.bpl b/Test/bitvectors/bv10.bpl new file mode 100644 index 00000000..7c325d95 --- /dev/null +++ b/Test/bitvectors/bv10.bpl @@ -0,0 +1,10 @@ +var x: bv32;
+
+procedure main()
+modifies x;
+{
+
+ x := 0bv32;
+ assume x == 1bv32;
+ assert false;
+}
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
)
|