The current deterministic values parser in kani-driver/src/exe_trace.rs works on arbitrary serde::Value types. This means that if we expect certain Value blobs to be arrays, we have to test for that and handle errors. With this change, we would complete the serde struct for traces in kani-driver/src/cbmc_output_parser.rs and use those objects directly. We would still have to walk down this structure to extract deterministic values, but we wouldn't need as much error handling since the blob would be automatically serialized into the right type.