summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/issue3947-agg-miniscope.smt2
blob: c8e2db922b1913a67092001eb332c0aef6d8e448 (plain) 
1
2
3
4
5
6
7
8
9

; EXPECT: sat
; COMMAND-LINE: --sygus-inference
(set-logic ALL)
(set-option :ag-miniscope-quant true)
(set-option :sygus-inference true)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ((c Real)) (or (< c a) (< 0 b))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback