Apply SAW Core substitution to SAW Core term equalities.

[andreistefanescu]

A call f(0, 1, 2) fails to match an override with the spec

let f_spec = do {
  x <- llvm_fresh_var "x" (llvm_int 32);
  llvm_execute_func [(crucible_term {{ x - 1 }}), (crucible_term x), (crucible_term {{ x + 1 }})];
  crucible_return (crucible_term {{ 3 * x }});
};

because x -> 1 is not substituted in the assertion 0 == x - 1. This change collects all equalities (without asserting), then applies the entire substitution, and then asserts the equalities.

[brianhuffman]

@andreistefanescu, I can't tell what problem this is meant to solve; could you give me a bit of context?

[atomb]

I'm wondering about the same question. I'm not sure I really understand what it's for.

[andreistefanescu]

@atomb @brianhuffman I updated the description

[atomb]

Thanks for the explanation. This looks good to me!

[brianhuffman]

Why was a flexdis86 submodule update part of this PR? And to a non-master commit?