Rafael Sá Menezes

> off-topic: Rafael, do you think we can extend your vector code so we can support complex data type? I guess a vector[2] and a complex data type share several...

> The operations should be distributed between the real and img parts, just like vectors. I see, yes it should be straightforward.

Closed via #845

@lucasccordeiro were you able to contact @jmorse?

> . Are we disabling constant propagation for that variable? For instance, do we expect to see stuff like in following in the cex? Constant propagation should still work. It...

This PR has the following results: Statistics: 15648 Files correct: 8444 correct true: 5127 correct false: 3317 incorrect: 53 incorrect true: 24 incorrect false: 29 unknown: 7151 Score: 12339 (max:...

@mikhailramalho Is there a reason for not converting `__ESBMC_assert` or `__VERIFIER_assert` into an GOTO assertion?

> __VERIFIER_assert is actually a function in SV-COMP that eventually calls abort, e.g., Since is only a wrapper for a `reach_error`, it may be better to convert it to an...

> Could you please clarify? Which fenv.h, ESBMC's or macOS's? macOS's, we can't generate clibs in the current state. > Did you try -mfloat-abi=soft or -mfloat-abi=hard Just tried, `unsupported option...

@fbrausse I am not sure what I should execute ``` clang -v -m32 Apple clang version 13.1.6 (clang-1316.0.21.2.5) Target: arm-apple-darwin21.5.0 Thread model: posix InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin ```