blob: 98d75d74f67210be6ec7a1b5cc1c6c30401ba02a (
plain)
1
2
3
4
5
6
7
8
9
10
|
; COMMAND-LINE: --bv-solver=simple
; EXPECT: unsat
(set-logic ALL)
(declare-const __ (_ BitVec 3))
(declare-const ___ (_ BitVec 3))
(assert (= (_ bv0 64) (bvand (_ bv1 64) ((_ zero_extend 32) ((_ zero_extend 16) ((_ zero_extend 8) ((_ zero_extend 4) ((_ zero_extend 1) __))))))))
(assert (bvule __ ___))
(assert (= (_ bv0 64) (bvand (_ bv1 64) (bvadd (_ bv1 64) ((_ zero_extend 32) ((_ zero_extend 16) ((_ zero_extend 8) ((_ zero_extend 4) ((_ zero_extend 1) ___)))))))))
(assert (bvule ___ __))
(check-sat)
|
