Important bugs fixing

These changes are separated from my work on the pattern matcher. I finally manage to identify the reason why it breaks the matching logic prover.

Once this pull request gets merged, we should also apply the change in https://github.com/kframework/c-semantics/pull/39 again.

@dwightguth @andreistefanescu please review