Couple of issues with latest Z3

[evmaus]

Hey:

We're running into a couple of issues with the latest version of Z3 caught by TSAN and ASAN.

• There's a race condition in the logging code, which can be caught by TSAN. Here's two stack traces demonstrating the issue:

   #0 ~z3_log_ctx third_party/z3/src/api/api_log_macros.h:11:142 
    #1 Z3_mk_context_rc third_party/z3/src/api/api_context.cpp:345:9 
    #2 init third_party/z3/src/api/c++/z3++.h:159:21 
    #3 z3::context::context() third_party/z3/src/api/c++/z3++.h:170:31 

and

    #0 ~z3_log_ctx third_party/z3/src/api/api_log_macros.h:11:142
    #1 Z3_params_set_bool third_party/z3/src/api/api_params.cpp:70:9
    #2 set third_party/z3/src/api/c++/z3++.h:472:44 

• There's the potential for an integer overflow in src/util/mpz.cpp, around line 275, which can be caught with ASAN. Code in question is:

SASSERT(capacity(c) >= m_init_cell_capacity);
uint64_t _v;
if (v < 0) {
   _v = -v; // Overflows if v = INT_MIN before assignment
    c.m_val = -1;
}
else {
   _v = v;
    c.m_val = 1;

We're also running into a few cases where it appears to hang indefinitely (or at least for 15 minutes) and doesn't time out in a single threaded solving context, on problems it succeeded on quickly using a drop from April/May. I'm working on a repro--what would be helpful to help diagnose that sort of problem? I believe we're primarily using bools, bitvectors, and strings in the case where it hangs--I can potentially get a code sample that demonstrates the issue (we're using the API), or if I can get a repro via SMT2 terms, then an SMT2 representation of the crash.

Thanks,
Everett Maus

[NikolajBjorner]

1. race condition is benign, but I will update the scripts to use atomics. The log should not be used in concurrent mode so m_prev will always be false. Separate push will take care of this.

2. overflow doesn't show up under Windows, but surely C standard has it undefined behavior so this is now fixed. Pull request seems not correct because the unsigned interpretation of min-int64 would not correspond to -2^63 as far as I can tell. At any rate, added unit test for this case.

3. Non-termination regression can be diagnosed either using SMT2 file (easiest preferred) or a z3-log (Z3_open_log(..), which requires the API functions to be fixed, otherwise the log will not replay correctly). The log will not print nice things, but I can instrument the solver in ad-hoc ways to extract information unless existing verbose mode or logging or profiling already shows what is going on.

[NikolajBjorner]

added atomics to quell race condition flags, dealt with overflow issue.