Disconnecting terminator should be allowed in all solver states

[sfiruch]

I just encountered a problem I cannot reproduce:

cadical: fatal error: invalid API usage of 'void __cdecl CaDiCaL::Solver::disconnect_terminator(void)' in 'C:\Users\de\OneDrive - iru.ch\Source\cadical\src\solver.cpp': solver in invalid state

This is caused by the call to REQUIRE_VALID_STATE (); in https://github.com/arminbiere/cadical/blob/e71bd58937e6513f71bd8c93d91578785c592721/src/solver.cpp#L841C3-L841C23:

void Solver::disconnect_terminator () {
  LOG_API_CALL_BEGIN ("disconnect_terminator");
  REQUIRE_VALID_STATE ();
#ifdef LOGGING
  if (external->terminator)
    LOG ("disconnecting previous terminator");
  else
    LOG ("ignoring to disconnect terminator (no previous one)");
#endif
  external->terminator = 0;
  LOG_API_CALL_END ("disconnect_terminator");
}

I tried disconnecting the terminator after ccadical_solve returned. Perhaps it was a race-condition, an out-of-memory situation or something else. In any case: I think disconnecting terminators should be allowed in all solver states.

[arminbiere]

Hmm, probably a race (as 'terminator' is not really locked nor even volatile accessed in 'External'). Do you call the disconnection function from a signal handler or another thread? The later looks like a real race on your side. The former is something were we could drop the 'REQUIRE_VALID_STATE' contract checking.

[sfiruch]

The call is from the main thread, after ccadical_solve returns, potentially as part of exception handling. At this point in time, no CaDiCaL code is running anymore, but CaDiCaL's internal state might be inconsistent, due to e.g. a failing memory allocation (?). I would've expected the call to succeed in this case.

It's not a critical problem, and I can work around the problem. Feel free to ignore this report.

[arminbiere]

I am ignoring this for now.