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)