Fix SMTDefinable instances for 8-arg through 12-arg uninterpreted functions

[octalsrc]

The SMTDefinable instances for 8-arg through 12-arg uninterpreted functions feed arguments to the newUninterpreted function in the wrong order. The result is that, when such functions are used in a solver query, the solver returns an error at runtime.

For example, when using a function that takes arguments of types A1-A8 and returns Bool:

Exception:
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (define-fun s10 () Bool (f8 s0 s2 s3 s4 s5 s6 s7 s8))
***    Expected  : success
***    Received  : (error "line 34 column 51: unknown constant f8 (A1 A2 A3 A4 A5 A6 A7 A8)
***                declared: (declare-fun f8 (A2 A3 A4 A5 A6 A7 A8 Bool) A1) ")
***
***    Exit code : ExitFailure (-15)
***    Executable: /home/octal/.nix-profile/bin/z3
***    Options   : -nw -in -smt2
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

Use -p '/Uninterpreted.Function/&&/aufunc-8/' to rerun this test only.

This PR adds simple tests for uninterpreted functions that catch this error, and fixes the 8-arg through 12-arg instances.

Thanks so much for adding the higher-argument function instances I asked about in #670! I just now got back to what I needed them for, and encountered this bug, but it was an easy fix.

[LeventErkok]

Fantastic! Thank you for the patch.