From 75cdf16714372ec03f1697450c135acdd3df9db3 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 29 Sep 2009 06:39:10 +0000
Subject: Fixed some bugs in the generation of bitvector input for Z3.
 Deleted/ignored some binaries in the Binaries directory.

---
 Test/bitvectors/bv8.bpl | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 Test/bitvectors/bv8.bpl

(limited to 'Test/bitvectors/bv8.bpl')

diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl
new file mode 100644
index 00000000..7295f684
--- /dev/null
+++ b/Test/bitvectors/bv8.bpl
@@ -0,0 +1,23 @@
+// This file includes some tests for which Boogie once generated bad Z3 input
+
+procedure foo()
+{
+  var r: bv3;
+  var s: bv6;
+  var u: bv15;
+  var t: bv24;
+
+  t := t[8: 0] ++ t[10: 0] ++ t[24: 18];
+  t := (r ++ s) ++ u;
+  t := t[16: 0] ++ t[8: 0];
+}
+
+procedure bar()
+{
+  var a: bv64;
+  var b: bv32;
+  var c: bv8;
+
+  c := a[8:0];
+  c := b[8:0];
+}
-- 
cgit v1.2.3