test/regress/regress1/quantifiers/issue3765-quant-dd.smt2


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

; COMMAND-LINE: --finite-model-find --no-check-models
; EXPECT: sat

(set-logic ALL)

(declare-sort U 0)
(declare-fun g (U) Int)
(declare-sort V 0)
(declare-fun f (V) Int)
(assert (and 
(forall ((?i U)) (not (forall ((?z V)) (not (= (f ?z) (div (- 1) (g ?i))))) ))
))

(declare-fun k () U)
(assert (= (g k) 22))


(check-sat)