blob: 05639337d9b0b8be88128fab8301163257e81a0c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
; COMMAND-LINE: --dump-instantiations --print-inst=num --no-print-inst-full
; EXPECT: unsat
; EXPECT: (num-instantiations myQuantP 1)
; EXPECT: (num-instantiations myQuantQ 7)
(set-logic UFLIA)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(assert (forall ((x Int)) (! (P x) :qid |myQuantP|)))
(assert (forall ((x Int)) (! (=> (Q x) (Q (+ x 1))) :qid |myQuantQ|)))
(assert (Q 0))
(assert (or (not (P 5)) (not (Q 7))))
(check-sat)
|
