If memory isn't zero-initialized the solver might get stuck

[stbrumme]

Hi Marijn,
depending on the compiler optimization level, memory isn't always initialized to zero.
If the values of m_false[0] and m_prev[0] happen to be non-zero, the following lines might create an infinite loop
as soon as the decision variable becomes zero (depends on S->prev[0], too):

microsat/microsat.c

Lines 173 to 174 in 04f9625

	while (S->false[decision] || S->false[-decision]) { // As long as the temporay decision is assigned
	decision = S->prev[decision]; } // Replace it with the next variable in the decision list

Proposed fix:
set m_false[0] = 0; in initCDCL()

[rokicki]

I have observed this too. Please use calloc() instead of malloc(). I propose fixing this by using

  S->DB = (int *) calloc (sizeof (int), S->mem_max); // Allocate the initial database

instead of the malloc line.