printf -> model_print

printf -> model_print

As we move toward redirecting program output, we will need a special
printf function for model-checking prints. Just define a simple
model_print() for now.