summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2
blob: 73c278522ae945bc477199b5f780c259afab8bf7 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

(set-logic LRA)
(set-info :status unsat)
(declare-fun a () Real)
(assert 
  (forall ((?y2 Real) (?y3 Real)) 
    (or 
        (= ?y3 1) 
        (> ?y3 0)
        (and 
          (< ?y2 0) 
          (< ?y3 49) 
        )))
)
(check-sat)
(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback