blob: 7e1cd80b30b901a8d3077b5d22c158a1efe2bdcb (
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 --uf-ho
(set-logic ALL)
(declare-var uf (-> Int Int))
(synth-fun f ((x Int) (y Int)) Bool
((Start Bool) (IntExpr Int))
((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)
|
