Caching swallows counterexamples

[aterga]

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. ([email protected])"
          }
        ],
        "type": "error"
      },
      "time": 0
    },
    "kind": "for_entity",
    "status": "failure",
    "verifier": "silicon"
  },
  "msg_type": "verification_result"
}