summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/issue3514.smt2
blob: dd6011df92a3702347074d06f3c9e58834df80da (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

; EXPECT: sat
; COMMAND-LINE: --sygus-inference
(set-logic ALL)
(assert
 (forall ((a Real))
  (exists ((b Real))
   (exists ((c Real))
    (and
     (< (+ a c) 0.0)
     (or (distinct a 0.0) (= b 5.0))
     (distinct (+ b c) 1.0)
     (< c 1))))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback