Define the difference between Plain Symbols and Nullary UFs.

[kfriedberger]

All solvers allow to define nullary UFs, i.e., UFs without arguments. For some solvers, the returned formula can be used just like a plain symbol/variable and is even comparable, i.e. identical. For other solvers, a nullary UF is different from a plain symbol and appears to be a separate object.

We should document, which solvers allow this and provide more tests for this (see fb0de870f61047f92ce872d3718bce6c4673872f). Or we could return plain variables when requesting a nullary UF (or vice versa).