blob: 66880eafa17d8315eeef29723621f3552a9dcf5e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --uf-ho
(set-logic UFLIA)
(declare-fun uf ( Int ) Int)
(synth-fun f ((x Int) (y Int)) Bool
((Start Bool (true false
(<= IntExpr IntExpr )
(= IntExpr IntExpr )
(and Start Start )
(or Start Start )
(not Start )))
(IntExpr Int (0 1 x y
(+ IntExpr IntExpr )
(- IntExpr IntExpr )))))
(declare-var x Int)
(constraint (f (uf x) (uf x)))
(constraint (not (f 3 4)))
(check-synth)
|
