Software Model Checking via Large-Block Encoding.