Value mismatch between CBMC's console log and GraphML witness

[Po-Chun-Chien]

CBMC prints the values for __VERIFIER_nondet in both its console logs and GraphML witnesses when an error path is found.
However, sometimes these values do not match.

Here is an example.

• Program: cambridge.2.prop1-back-serstep.c
• Property: unreach-call.prp
• CBMC version: 5.70.0-121-g4f69955d00 (binaries and wrapper script downloaded from tool archive of SV-COMP 2023)
• Command line:

  ./cbmc --graphml-witness witness.graphml --propertyfile unreach-call.prp --64 cambridge.2.prop1-back-serstep.c > exe.log

The input and output files are also available here: example.zip

The values for input_149 = __VERIFIER_nondet_ushort() at line 181 of the program in exe.log and witness.graphml mismatch, as shown by

$ grep "input_149=" exe.log 
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=0 (00000000 00000000)
  input_149=65535 (11111111 11111111)
  input_149=65535 (11111111 11111111)
  input_149=65535 (11111111 11111111)

$ grep -A 2 '<data key="startline">181</data>' witness.graphml 
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>
--
      <data key="startline">181</data>
      <data key="threadId">0</data>
      <data key="assumption">\result = 0;</data>

Both files contain 11 occurrences of input_149.
However, the values are different in the last 3 loop iterations (65535 vs. 0).