blob: a107fd88b78d99446202ffa683f0f8abf6da5245 (
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
|
; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const
; 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)
(synth-fun g ((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
; and arguments 1...3, 5...10 are irrelevant for g
(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7)))
(constraint (>= (g x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x4 x4 x4)))
(check-synth)
|
