Caching swallows counterexamples

When ViperServer retrieves and reports cached verification failures, it should also report the counterexamples that were produced for the cached verification attempts. Currently, this is not the case.

To reproduce, start ViperServer as usual, copy the port number, and send the following verification requests using viper_client — twice:

./client.py -p 54292 -f /Users/wi/viper/viper_client/models/test.vpr -x "--counterexample native"

After the first run, you'll see a response that starts like this:

{
  "msg_body": {
    "details": {
      "result": {
        "errors": [
          {
            "cached": false,
            "counterexample": {
              "model": {
                "$FVF.loc_FIELD_VAL": {
                  "cases": [],
                  "default": {
                    "type": "constant_entry",
                    "value": "true"
                  },
                  "type": "map_entry"
                },
         ...

After the second run, the entire verification result will be just this:

{
  "msg_body": {
    "details": {
      "cached": true,
      "entity": {
        "name": "test",
        "position": {
          "end": "13:1",
          "file": "/Users/wi/viper/viper_client/models/test.vpr",
          "start": "3:12"
        },
        "type": "method"
      },
      "result": {
        "errors": [
          {
            "cached": false,
            "position": {
              "end": "10:9",
              "file": "/Users/wi/viper/viper_client/models/test.vpr",
              "start": "10:8"
            },
            "tag": "assert.failed:assertion.false",
            "text": "Assert might fail. Assertion (NODE_X.FIELD_VAL in FOOTPRINT) might not hold. (test.vpr@10.8--10.9)"
          }
        ],
        "type": "error"
      },
      "time": 0
    },
    "kind": "for_entity",
    "status": "failure",
    "verifier": "silicon"
  },
  "msg_type": "verification_result"
}

Start ViperServer and use the viper_client command from the issue twice with --counterexample native. Compare the first and cached verification_result responses, then trace the cached-result retrieval path. Done means the second response reports the counterexample data as well as the verification failure.