blob: 1d724139950c673e7261353338000b441cc17124 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
(synth-fun inv ((s (_ BitVec 4)) (t (_ BitVec 4))) (_ BitVec 4))
(declare-var s (_ BitVec 4))
(declare-var t (_ BitVec 4))
(define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
(ite (= b #x0) #xF (bvudiv a b))
)
(define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
(ite (= b #x0) a (bvurem a b))
)
(define-fun min () (_ BitVec 4)
(bvnot (bvlshr (bvnot #x0) #x1))
)
(define-fun max () (_ BitVec 4)
(bvnot min)
)
(define-fun l ( (s (_ BitVec 4)) (t (_ BitVec 4))) Bool
(= (udivtotal s (inv s t)) t)
)
(define-fun SC ((s (_ BitVec 4)) (t (_ BitVec 4))) Bool
(= (udivtotal s (udivtotal s t)) t)
)
(constraint
(=>
(SC s t)
(l s t)
)
)
(check-synth)
|
