diff options
Diffstat (limited to 'test/regress/regress0/sygus/process-10-vars.sy')
-rw-r--r-- | test/regress/regress0/sygus/process-10-vars.sy | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/process-10-vars.sy b/test/regress/regress0/sygus/process-10-vars.sy new file mode 100644 index 000000000..523abd70d --- /dev/null +++ b/test/regress/regress0/sygus/process-10-vars.sy @@ -0,0 +1,24 @@ +; 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) + + +(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) + |