diff options
author | MichalMoskal <unknown> | 2011-02-18 22:04:41 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2011-02-18 22:04:41 +0000 |
commit | 2e4c60cba8c332250ee1a88fa62744eec0034763 (patch) | |
tree | 72437dcbc6a126d29e91bb0763d858352a2eaafc /Test/inline/expansion4.bpl | |
parent | 68b4c9c855b8d23e0bdc19078ba4a15eb48297b2 (diff) |
Remove a testcase for bvInt (feature to be killed soon)
Diffstat (limited to 'Test/inline/expansion4.bpl')
-rw-r--r-- | Test/inline/expansion4.bpl | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/Test/inline/expansion4.bpl b/Test/inline/expansion4.bpl deleted file mode 100644 index 593fa9fb..00000000 --- a/Test/inline/expansion4.bpl +++ /dev/null @@ -1,31 +0,0 @@ -function f(x:int) returns(bool);
-axiom {:ignore "bvInt"} {:inline true} (forall x:int :: f(x) <==> true);
-axiom {:ignore "bvDefSem"} {:inline true} (forall x:int :: f(x) <==> false);
-
-procedure {:forceBvZ3Native true} foo()
-{
- assert f(3);
-}
-
-procedure {:forceBvInt true} foo2()
-{
- assert !f(3);
-}
-
-axiom (forall x: bv64, y: bv64 :: { $sub.unchk.u8(x, y) } $check.sub.u8(x, y) ==> $sub.u8(x, y) == $sub.unchk.u8(x, y));
-axiom {:inline true} {:ignore "bvDefSem"} (forall x: bv64, y: bv64 :: { $check.sub.u8(x, y) }
-$check.sub.u8(x, y) <==> $_inrange.u8($sub.i8(x, y)));
-
-function $check.sub.u8(x: bv64, y: bv64) returns (bool);
-function $_inrange.u8(bv64) returns (bool);
-function {:bvbuiltin "bvsub"} $sub.unchk.u8(x: bv64, y: bv64) returns (bv64);
-function {:bvbuiltin "bvsub"} {:bvint "-"} $sub.i8(x: bv64, y: bv64) returns (bv64);
-function {:bvbuiltin "bvsub"} {:bvint "-"} $sub.u8(x: bv64, y: bv64) returns (bv64);
-
-
-procedure {:forceBvZ3Native true} baz()
-{
- return;
-}
-
-
|