test/regress/regress0/push-pop/inc-double-u.smt2


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

; COMMAND-LINE: --incremental 
(set-logic UFLIA)
(declare-fun P (Int) Bool)
(declare-fun R (Int) Bool)
(assert (forall ((x Int)) (=> (R x) (not (P x)))))
; EXPECT: unknown
(check-sat)
(assert (R 0))
; EXPECT: unknown
(check-sat)
(assert (forall ((x Int)) (P x)))
; EXPECT: unsat
(check-sat)
(push 1)
; EXPECT: unsat
(check-sat)