When looking at a CBMC witness from SV-COMP, one can see that there are several circumstances where CBMC adds invalid assumptions that violate the rules of the witness format for assumption and assumption.scope.

1. Initializations of global variables are declared to be in the scope of a non-existing function __CPROVER_initialize:

   <edge source="4079.19" target="4082.302">
     <data key="originfile">../../sv-benchmarks/c/aws-c-common/aws_byte_buf_cat_harness.i</data>
     <data key="startline">8915</data>
     <data key="threadId">0</data>
     <data key="assumption">errors[0l].error_code = 0;</data>
     <data key="assumption.scope">__CPROVER_initialize</data>
   </edge>
   

   Here, assumption.scope should be removed.

2. There are assumptions declared for internals of extern functions like malloc, referencing non-existing variables:

   <edge source="2834.362" target="355.384">
     <data key="originfile">../../sv-benchmarks/c/aws-c-common/aws_byte_buf_cat_harness.i</data>
     <data key="startline">6960</data>
     <data key="threadId">0</data>
     <data key="assumption">malloc_size = 4ul;</data>
     <data key="assumption.scope">malloc</data>
   </edge>
   

   These should be removed.

3. There are assumptions referencing local variables that are out of scope:

   <edge source="21.389" target="2196.393">
     <data key="originfile">../../sv-benchmarks/c/aws-c-common/aws_byte_buf_cat_harness.i</data>
     <data key="startline">9136</data>
     <data key="threadId">0</data>
     <data key="assumption">buf = &amp;buffer1;</data>
     <data key="assumption.scope">aws_byte_buf_is_valid</data>
   </edge>
   

   The only occurrence of buffer1 in this program is as a local variable of aws_byte_buf_cat_harness. This is the variable whose address ends up in buf, so it is understandable where this assumption comes from, but it is not possible to express this in the current witness format and the assumption should be removed.

In practice, a witness validator might ignore assumptions with invalid scopes or variable names, but especially in the last case it could easily happen that due to naming clashes between variables of different functions a syntactically valid but semantically invalid assumption is created and the witness is rejected (in the example, aws_byte_buf_is_valid just would need to have another parameter named buffer1).

The same problems exist for invariants added to correctness witnesses in the invariant and invariant.scope fields.

CBMC version: the one of SV-COMP'20, problem still occurs in CBMC 5.12
Operating system: Ubuntu 18.04 (SV-COMP environment)
Exact command line resulting in the issue: ./cbmc --graphml-witness witness.graphml --64 --propertyfile ../../sv-benchmarks/c/properties/unreach-call.prp ../../sv-benchmarks/c/aws-c-common/aws_byte_buf_cat_harness.i