GCC 4.92 miscompiles Z3. I've tried Cygwin and Linux, 32 and 64 bits, and all miscompile.
Sorry, a bit more information the problem: On function void reduce_args_tactic::imp::populate_decl2args_proc::operator()(app * n), when compiled with -O0 no call to memory::deallocate(void* p) is made, while with -O2 memory::deallocate is called with p == 0, which cannot happen (since it's called through dealloc_svect, which bails out if the pointer is null). Apologies for not being able to reduce the test case; I don't have much experience with the gcc internals.
Created attachment 35465 [details] test case
Created attachment 35467 [details] reduced test case
(In reply to Nuno Lopes from comment #3) > Created attachment 35467 [details] > reduced test case The reduced testcase is compiled correctly in that the deallocate is called unconditional with zero argument: bit_vector() : m_num_bits(0), m_capacity(0), m_data(0) { memory::deallocate(m_data); } m_data will be NULL always when deallocate is called.
Created attachment 35514 [details] Reduced test case Previous reduced test case was bogus. This one should be ok.
Note even though the length that is passed to memcpy is zero, the arguments have to be non-null. So adding the check around the call to memcpy should fix the issue.
Basically GCC understands that memcpy takes non-null arguments and optimizes based on that.