summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/large-const-simp.sy
blob: 08f280a4ba796cc15acc9d0dda9fdb5202895767 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-add-const-grammar
(set-logic LIA)

(synth-fun lc ((x Int)) Int)

(declare-var x Int)
(declare-var y Int)

(constraint (> (lc x) 1500))
(constraint (< (lc x) 1600))

(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback