diff options
Diffstat (limited to 'test/regress/regress0/bv/smtcompbug.smt')
| -rw-r--r-- | test/regress/regress0/bv/smtcompbug.smt | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/smtcompbug.smt b/test/regress/regress0/bv/smtcompbug.smt new file mode 100644 index 000000000..7efe3015c --- /dev/null +++ b/test/regress/regress0/bv/smtcompbug.smt @@ -0,0 +1,13 @@ +(benchmark B_ + :status sat + :category { unknown } + :logic QF_BV + :extrafuns ((x781 BitVec[32])) + :extrafuns ((x803 BitVec[8])) + :extrafuns ((x804 BitVec[8])) + :extrafuns ((x791 BitVec[8])) + :formula (and +(= x804 (bvxor (bvxor (extract[7:0] (bvadd bv1[32] x781)) x791) x803)) +(= (bvnot (extract[0:0] x804)) bv0[1]) +(= x781 bv0[32])) +) |