blob: 1f383ab4301612967b5ab26412804c06cfeab7e9 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool
(or
(= v1 z)
(= v2 z)))
(synth-fun f ((x0 Int) (x1 Int)) Bool
((Start Bool) (StartInt Int) (IntVar Int))
(
(Start Bool ( (letf StartInt IntVar IntVar) ))
(StartInt Int (5))
; "Hack" to avoid parse errors in V2 format.
(IntVar Int ((Variable Int)))
)
)
(declare-var a Int)
(declare-var b Int)
(constraint (=> (= a 5) (f a b)))
(constraint (=> (= b 5) (f a b)))
(check-synth)
|
