test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2


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

; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk
; EXPECT: sat
(set-logic UFLIA)
(set-info :status sat)
(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool (
    or
    (= n1 n 0)
    (= n2 n 0)
    (
        and
        (> n1 0)
        (> n2 0)
        (>= n 0)
        (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0))))
        (int-and (div n 2) (div n1 2) (div n2 2))
    )
))
(check-sat)