diff options
Diffstat (limited to 'test/regress/regress2/sygus/process-arg-invariance.sy')
| -rw-r--r-- | test/regress/regress2/sygus/process-arg-invariance.sy | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/process-arg-invariance.sy b/test/regress/regress2/sygus/process-arg-invariance.sy new file mode 100644 index 000000000..3c18b6c75 --- /dev/null +++ b/test/regress/regress2/sygus/process-arg-invariance.sy @@ -0,0 +1,18 @@ +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar +; 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 x Int) +(declare-var y Int) + +; should be able to determine that only 3 arguments +; (one of 5...9, one of 1 or 4, one of 2 or 3) is relevant for f + +(constraint (> (f (+ x x) (+ x 1) (+ x 1) (+ x x) x x x x x 0) (+ x x x))) +(constraint (<= (f x x x x x x x x x 0) (+ x x x))) + +(check-synth) + |