Linear Unification based on C-expressions