improve lhs/rhs

give errors if sympy object has no .lhs or .rhs attribute
documentation: add lhs/rhs to thing we have, SMT doesn't
children: improve documentation

Fixes #139.