1 files changed, 9 insertions, 0 deletions
diff --git a/Test/bitvectors/bv6.bpl b/Test/bitvectors/bv6.bpl
new file mode 100644
index 00000000..ca8f8367
--- /dev/null
+++ b/Test/bitvectors/bv6.bpl
@@ -0,0 +1,9 @@
+
+procedure Q() returns () {
+  var x : bv32, y : bv16;
+
+  x := y ++ y;
+  assert x[16:0] == y;
+  assert x == x[16:0] ++ y;
+  assert x[17:1] == y;     // should not be verifiable
+}
+\ No newline at end of file