First more or less stable version of SOS with our own SMT solver and with support of invariants.
Version after diploma thesis completition