test/regress/regress0/sygus/hd-sdiv.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=none --no-dump-synth
(set-logic BV)

(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))

(synth-fun f ((x (BitVec 32))) (BitVec 32)
    ((Start (BitVec 32) ((bvsdiv Start Start)
						             (bvand Start Start)
                         x
                         #x00000001))))

(declare-var y (BitVec 32))
(constraint (= (hd01 y) (f y)))
(check-synth)