blob: 88ddcf1397dd8e57897954e1e8f48d0359910f06 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
; EXPECT: unsat
; COMMAND-LINE: --no-dump-synth
(set-logic BV)
(define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
(let ((modulo-shift (BitVec 32) (bvand bit #x0000001f)))
(bvand modulo-shift x)))
(synth-fun btr ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
((Start (BitVec 32) (
(Constant (BitVec 32))
(Variable (BitVec 32))
(bvneg Start) (bvnot Start) (bvadd Start Start) (bvand Start Start) (bvlshr Start Start) (bvmul Start Start) (bvor Start Start) (bvshl Start Start)
))))
(declare-var x (BitVec 32))
(declare-var bit (BitVec 32))
(constraint (= (btr x bit) #b00000000000000000000000000000000))
(check-synth)
|
