test/regress/regress2/sygus/array_sum_dd.sy


1
2
3
4
5
6
7
8
9
10
11

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
(synth-fun findSum ( (y1 Int) (y2 Int) )Int (
(Start Int ( 0 1 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) 
(BoolExpr Bool ((< Start Start) (<= Start Start)))))
(declare-var x1 Int)
(declare-var x2 Int)
(constraint (=> (> (+ x1 x2) 0) (= (findSum x1 x2 ) x1)))
(constraint (=> (<= (+ x1 x2) 0) (= (findSum x1 x2 ) x2)))
(check-synth)