summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2
blob: 6379d6cece65364a93923d57e2d989c5f037ebad (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

; COMMAND-LINE: --cbqi-nested-qe
; EXPECT: unsat
(set-logic LRA)

(declare-fun c () Real)

(assert 
(forall ((?x2 Real)) 
(exists ((?x3 Real)) 
(and
(forall ((?x4 Real)) (or 
(not (>= ?x4 4)) 
(and (> c (+ ?x2 ?x3)) (> (+ c ?x3 ?x4) 0))) )
(not (> (+ c ?x2 ?x3) 0)) )
)) )

(check-sat)
(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback