summaryrefslogtreecommitdiff
path: root/test/regress/regress1/abduction/abd-real-const.smt2
blob: 258d80a88bd4d15fcbd28344ac0e11ec6185d863 (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --produce-abducts
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
(set-logic QF_LRA)
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (and (>= x 0) (< y 7)))
(get-abduct A (>= y 5))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback