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

; COMMAND-LINE: --cegqi-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