diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-07-09 13:17:17 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-07-09 13:17:17 -0700 |
| commit | d96c9e3ca3eca81e35821261bdb1fee446f8013e (patch) | |
| tree | d51a1f3d5cd17dcd85b38553fc19be22eea2de23 | |
| parent | 0251bc077fbfce58f0fa80dc04ba2ee8088f2686 (diff) | |
added a new regression
| -rw-r--r-- | Test/bitvectors/bv10.bpl | 10 |
1 files changed, 10 insertions, 0 deletions
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;
+}
|