diff options
Diffstat (limited to 'test/regress/regress0/bv/core/equality-02.smt')
| -rw-r--r-- | test/regress/regress0/bv/core/equality-02.smt | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/core/equality-02.smt b/test/regress/regress0/bv/core/equality-02.smt new file mode 100644 index 000000000..ee011ceb4 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-02.smt @@ -0,0 +1,20 @@ +(benchmark B_ + :status unsat + :logic QF_BV + :extrafuns ((x0 BitVec[32])) + :extrafuns ((x1 BitVec[32])) + :extrafuns ((x2 BitVec[32])) + :extrafuns ((x3 BitVec[32])) + :extrafuns ((y0 BitVec[32])) + :extrafuns ((y1 BitVec[32])) + :extrafuns ((y2 BitVec[32])) + :extrafuns ((y3 BitVec[32])) + :assumption (= x0 x1) + :assumption (= x1 x2) + :assumption (= x2 x3) + :assumption (= y0 y1) + :assumption (= y1 y2) + :assumption (= y2 y3) + :assumption (= x0 y0) + :formula (not (= x3 y3)) +) |