summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/interpol3.smt2
blob: 8681acf3a0aaec1ba896795de679fda5d181d7ae (plain) 
1
2
3
4
5
6
7

; COMMAND-LINE: --produce-interpols=default --check-interpols
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
(set-logic LIA)
(declare-fun a () Int)
(assert (> a 1))
(get-interpol A (> a 0))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback