diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 23:39:25 -0400 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 23:39:25 -0400 |
| commit | a8074075b507246379f7f24f2a13cc2340eb7fc9 (patch) | |
| tree | 0c63a6d61dc8bae22c00eaf7b85cd3f8c33f75b6 /test/regress | |
| parent | 170d322c39a72cb48dc892e71176862c473ae75b (diff) | |
fixed reversed concat in core theory
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/bv/core/slice-14.smt | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/bv/core/slice-14.smt b/test/regress/regress0/bv/core/slice-14.smt index b40f7938d..db3a3a7b3 100644 --- a/test/regress/regress0/bv/core/slice-14.smt +++ b/test/regress/regress0/bv/core/slice-14.smt @@ -1,8 +1,8 @@ (benchmark slice :status unsat :logic QF_BV - :extrafuns ((x BitVec[16])) - :assumption (= (extract[15:1] x) (extract[14:0] x)) + :extrafuns ((x BitVec[6])) + :assumption (= (extract[5:1] x) (extract[4:0] x)) :assumption (= (extract[0:0] x) bv0[1]) - :formula (not (= x bv0[16])) + :formula (not (= x bv0[6])) ) |