diff options
Diffstat (limited to 'test/regress/regress2/sygus/process-10-vars-2fun.sy')
| -rw-r--r-- | test/regress/regress2/sygus/process-10-vars-2fun.sy | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy new file mode 100644 index 000000000..00340030f --- /dev/null +++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy @@ -0,0 +1,28 @@ +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; 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) + |