Software Model Checking via IC3