blob: 1e810fea3f4a4f9980a957f50067b40527a96321 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-unif --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int
(
(Start Int
(0 1 x y
(+ Start Start)
(- Start Start)
(ite CBool Start Start)
)
)
(CBool Bool
(true false
(and CBool CBool)
(or CBool CBool)
(not CBool)
(<= Start Start)
; Having equality makes the problem easy to CEGIS
; (= Start Start)
)
)
)
)
(declare-var x Int)
(declare-var y Int)
(constraint (= (f 0 1) 0))
(constraint (= (f 1 y) y))
(constraint (= (f 2 1) 0))
(check-synth)
|
