Potential NULL pointer dereference in fun_solver_assign_base_values

[shaobo-he]

buffer is initialized to an empty vector and is then resized via resize_ivector. If p can be 0, then resize_ivector does nothing, causing buffer.data to be NULL.

The error trace starting from fun_solver_assign_base_values is attached. Bug7.txt

[BrunoDutertre]

Here's the code fragment that sets p:

      h = type_card(solver->types, sigma);
      p = i - m;
      if (p > h) p = h;

h is positive because there are no empty types in Yices and i is larger than m. So p can't be zero.