Hi Alastair,
Our assumption is that code should not be able to construct such
expressions in the first place and they are thus invalid at the KQuery
level. That expression is also invalid at the SMT level, as Concat
should take bitvectors and not booleans as arguments. If for some
reason
I am trying to chase down a bug that occurs while applying KLEE to a
multi-module Rust program (assembly.ll is approx 200k lines).
I'm hoping for suggestions of what might be wrong and/or how to narrow down
the cause of the bug.
What I am seeing in the stack trace is
that
