test/regress/regress1/fmf/fmf-fun-divisor-pp.smt2


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

; COMMAND-LINE: --fmf-fun
; EXPECT: unsat
(set-logic UFNIA)
(set-info :status unsat)
(define-fun-rec pow ((a Int)(b Int)) Int 
    (ite (<= b 0) 
         1 
         (* a (pow a (- b 1)))))

(declare-fun x () Int)

(assert (>= x 0))
(assert (< x (pow 2 2)))
(assert (>= (mod (div x (pow 2 3)) (pow 2 2)) 2))

(check-sat)