blob: b43c9697a58628f967d8b1ec5fc07f97fce43d58 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; COMMAND-LINE: --debug-inst --no-check-unsat-cores
; EXPECT: (num-instantiations myQuant1 1)
; EXPECT: (num-instantiations myQuant2 1)
; EXPECT: unsat
(set-logic UFLIA)
(declare-fun P (Int) Bool)
(declare-fun R (Int) Bool)
(declare-fun Q (Int) Bool)
(assert (forall ((x Int)) (! (=> (R x) (P x)) :qid |myQuant1|)))
(assert (forall ((x Int)) (! (=> (P x) (Q x)) :qid |myQuant2|)))
(assert (R 5))
(assert (not (Q 5)))
(check-sat)
|
