Eliminate redundant computation in VC experession translation

[shazqadeer]

This PR is in response to issue #993 which uncovers unexpected long-running execution during the translation of a large Expr into a VCExpr. My intuition suggested that the expression translation should do linear work unless the expression being translated involves deeply nested inlined function calls. Linear complexity would not exhibit the behavior being seen since the example does not have deeply nested function calls.

The root cause appears to be a piece of code that examines the current term substitution whenever the translation scope crosses a binding (let-binding or quantifier). This examination is done to collect free variables in the substituted expressions to check whether they might collide with the bound variables in the binding about to be translated. In the example, the function ConcatVec is being invoked with increasingly larger expressions for its arguments which makes the substitution mapping formals to actuals increasingly larger. There is a let binding inside ConcatVec which triggers the examination of the increasingly larger substitutions. This ultimately leads to quadratic complexity in translation.

I concluded that the collision detection is unnecessary because it will never detect any collisions in the scenarios where it is being invoked. The substitutions should never refer to the bound variables of the binding being translated. To test my understanding, I ran the Boogie tests with a Debug.Assert capturing my hypothesis. All tests passed.

This PR removes the redundant collision detection code.

[RustanLeino]

Your reasoning looks correct to me. That is, I agree that, for a well-formed Boogie program, no collision would be possible. So, it seems fine to remove that logic.

[shazqadeer]

Fixes issue #993