[sledge] Use fresh var for length when extracting from a variable
[sledge] Use fresh var for length when extracting from a variable

Summary:
When solving equations such as `α[o,l) = β`, the memory theory solver
computes a term to represent the length of α. This fails if α is a
variable (which might itself be equal to a sized term elsewhere in the
formula). This diff fixes such failures by generating a fresh variable
for the length in such situations.

Reviewed By: ngorogiannis

Differential Revision: D27564871

fbshipit-source-id: e5e066b77

facebook/infer,facebook/infer,jvillard/infer,jvillard/infer,jvillard/infer,jvillard/infer,facebook/infer,facebook/infer,jvillard/infer,facebook/infer,jvillard/infer,facebook/infer,facebook/infer,jvillard/infer