blob: 6a9a80a4938e30635f82bd49f411f1c9be2d8a3e (
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
|
; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-arg-relevant
; EXPECT: unsat
(set-logic LIA)
(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)
(declare-var x1 Int)
(declare-var x2 Int)
(declare-var x3 Int)
(declare-var x4 Int)
(declare-var x5 Int)
(declare-var x6 Int)
(declare-var x7 Int)
(declare-var x8 Int)
(declare-var x9 Int)
(declare-var x10 Int)
; should be able to determine that arguments 1...6, 8...10 are irrelevant for f
(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7)))
(check-synth)
|
