diff options
Diffstat (limited to 'test/regress/regress0/bv/sizecheck.cvc')
| -rw-r--r-- | test/regress/regress0/bv/sizecheck.cvc | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/sizecheck.cvc b/test/regress/regress0/bv/sizecheck.cvc new file mode 100644 index 000000000..e9326d9f6 --- /dev/null +++ b/test/regress/regress0/bv/sizecheck.cvc @@ -0,0 +1,7 @@ +x : BITVECTOR(10); +y : BITVECTOR(12); + +ASSERT (0bin0001000000000000 = BVPLUS(16, x, y)); +CHECKSAT; +% EXPECT: sat +% EXIT: 10 |