Zvonimir Rakamaric

Is this because LLVM maybe compiles away these assertions or something like that? What is the root cause of this? Is the generated Boogie file ok?

FYI, we have a similar issue with Rust, where `malloc` is called `je_mallocx`. Maybe the names we match should be regular expressions instead of just string constants.

I am a bit confused here. I just tried to pass `/z3opt:smt.mbqi=true` to Boogie, and Boogie fails to prove the quantified loop invariant. What am I missing? How exactly do...

Ok, when I turn on MBQI, then `array_forall_fail` times out. Also, what do you mean by "inlining an application of the identity function"?

Got it, thanks. Btw, do you observe the same timeout as me?

I think you probably meant "when the query is satisfiable". Hmmm, ok, so what should we do with this?

Why does it matter to SMACK what `long double` is in C? LLVM has `x86_fp80` type, and hopefully that is what we use in our source code to recognize it....

I agree with your point (2) above. My follow-up question is - do we have any regressions or are there any SVCOMP benchmarks that use `x86_fp80`?

Ah, I see. You were mainly referring to the naming convention in your point (1). Yes, I agree with that. The way I see it, we should: (1) Rename this...

Good point Mike. I would actually like to see something similar even for imprecise choices, such as for example our current implementation of inttoptr. Something like "WARNING: false bugs possible...