Mark S. Baranowski

Simple tests for correct realloc behavior. Attached as a .txt file since github rejects .c files. [realloc_simple.txt](https://github.com/smackers/smack/files/205571/realloc_simple.txt)

This was fixed quite some time ago. I'm not sure why it didn't get closed automatically.

Apparently it never got merged in...

I couldn't remember why I never made a PR for that branch, which is from June 2018. I realized that it's not quite right to completely remove the lower bound...

This program produces this intrinsic: ```c #include "smack.h" #include int main() { double f = __VERIFIER_nondet_double(); __VERIFIER_assume(!isnan(f)); __VERIFIER_assume(0.0 < f); __VERIFIER_assume(isfinite(f)); double z = fmodf(f, 2.0); __VERIFIER_assert(z

This one will take a while to track down. If I print the result of the function call before returning, then everything works correctly. This suggests some undefined behavior. I'll...

This occurs for all expressions of the form x \* sqrt(y), x/sqrt(y), sqrt(y)*x, sqrt(y)/x

The newest [version](https://github.com/soarlab/gelpia/commit/cbbe072d1bd3a66fa20a13ee245c07018cc6ce5f) appears to fix this issue. In the past I've seen Rust compiler issues with SIMD values where the result of a function (in the xmm0 register) has...

The old build.sh passed the --disable-preserve-rounding flag to configure while building GAOL. The new script in https://github.com/soarlab/gelpia/commit/99b9735ae89ffc683206cd622930409bb3fc4311 builds GAOL in the untrusted rounding mode. Historically, gelpia checked that the FP...

These functions are now present in gelpia (FPTaylorCompat) both the a\* and arc\* versions. What are your preferred ranges for arcsin and arccos? Gaol prefers [-pi/2,pi/2] for the former and...