summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/assume-simple.sy
blob: 58f3753d899d27af6f2c5abaf2c41e347bbdf388 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status

(set-logic LIA)
(synth-fun f ((x Int)) Int
  ((Start Int))
  ((Start Int (x 0 1 (+ Start Start)))))
(declare-var y Int)
(assume (>= y 0))
(constraint (>= (f y) 0))
(constraint (>= (f y) y))
; lambda x. x is a valid solution
(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback