Unexpected Clauses for SSA Expression

[luke-croak]

CBMC version: 5.28.0
Operating system: Ubuntu 20.04.3 LTS
Exact command line resulting in the issue: cbmc --slice-formula --write-solver-stats-to out.json code.c

What behaviour did you expect: I expected the formula to be sliced which I thought would remove unnecessary components from the CNF and not introduce new components to the CNF in comparison to running it without --slice-formula; i.e., cbmc --write-solver-stats-to out.json code.c.

What happened instead: It introduced clauses that corresponded to an SSA expressions of the form "true" which seemed to be used to refer to a GOTO statement. This was unexpected because:

1. It seemed to introduce clauses which didn't exist previously to capture the "true" SSA expression, and
2. The SSA expression "true" didn't make much sense to me as I thought the formula was formed by converting the expressions found in cbmc --show-vcc --slice-formula code.c into a SAT form, none of which have the expression "true", and
3. It also doesn't make much sense to me to have an SSA expression "true" for a GOTO statement. I wasn't aware of such a conversion.

With the --slice-formula option the output json file contains the following:

    {
        "GOTO": "GOTO 4",
        "GOTO_ID": 17088,
        "SAT_hardness": {
            "ClauseSet": [
                1,
                2,
                3
            ],
            "Clauses": 3,
            "Literals": 7,
            "Variables": 3
        },
        "SSA_expr": "true",
        "Source": {
            "file": "code.c",
            "function": "compare_arrays",
            "line": "225",
            "workingDirectory": (REMOVED)
        }
    }

The above SSA expression did not have any clauses associated with it when the program was run without --slice-formula.

Attached is the program from which this unexpected behaviour was generated.

code.zip