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

; EXPECT: unsat
; COMMAND-LINE: --cegqi-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