{
  "ana": {
    "apron": {
      "invariant": {
        "diff-box": true
      }
    }
  },
  "witness": {
    "yaml": {
      "enabled": true,
      "sv-comp-true-only": false,
      "entry-types": [
        "invariant_set",
        "ghost_instrumentation"
      ],
      "invariant-types": [
        "loop_invariant",
        "flow_insensitive_invariant"
      ]
    },
    "invariant": {
      "after-lock": false,
      "other": true,
      "accessed": false,
      "exact": true,
      "flow_insensitive-as": "invariant_set-location_invariant"
    }
  }
}
