Invariant check fails with --z3 and --json-ui

[zhassan-aws]

This test is the same one in #7185, but with an extra assert:

#include <assert.h>

struct Unit
{
};

int main() {
    struct Unit var_0;
    int x;
    int y = x;
    assert(0);
    assert(y == x);
    return 0;
}

Running it with --z3 and --json-ui causes an invariant violation:

$ cbmc unit2.c --z3 --json-ui
[
  {
    "program": "CBMC 5.69.1 (cbmc-5.69.1)"
  },
  {
    "messageText": "CBMC version 5.69.1 (cbmc-5.69.1) 64-bit x86_64 linux",
    "messageType": "STATUS-MESSAGE"
  },
  {
    "messageText": "Parsing unit2.c",
    "messageType": "STATUS-MESSAGE"

# -- snip --

          }--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/json_goto_trace.cpp:121 function: convert_decl
Condition: step.full_lhs_value.is_not_nil()
Reason: full_lhs_value in assignment must not be nil
Backtrace:
cbmc(+0xa8bde0) [0x559203cd5de0]
cbmc(+0xa8c389) [0x559203cd6389]
cbmc(+0x1e7d98) [0x559203431d98]
cbmc(+0x6853c6) [0x5592038cf3c6]
cbmc(+0x33d9f2) [0x5592035879f2]
cbmc(+0x357cac) [0x5592035a1cac]
cbmc(+0x1ef124) [0x559203439124]
cbmc(+0x1ee5fa) [0x5592034385fa]
cbmc(+0x1e5e2f) [0x55920342fe2f]
cbmc(+0x1d1e39) [0x55920341be39]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f8da07cc0b3]
cbmc(+0x1e77ae) [0x5592034317ae]


--- end invariant violation report ---
Aborted (core dumped)

This doesn't crash if I remove either of the --z3 or the --json-ui options.

CBMC version: 5.69.1
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc unit2.c --z3 --json-ui
What behaviour did you expect: Verification fails
What happened instead: CBMC crashed

[zhassan-aws]

Re-opening: I could reproduce the same invariant violation with CBMC 5.71.0 on a different program involving _Bool:

#include <assert.h>

int main(void)
{
    _Bool x = 1;

    assert(0);
    return 0;
}

$ cbmc --z3 nnn.c --json-ui
# -- snip --
          }--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/json_goto_trace.cpp:122 function: convert_decl
Condition: step.full_lhs_value.is_not_nil()
Reason: full_lhs_value in assignment must not be nil
Backtrace:
cbmc(+0xa7a7d0) [0x563f38c047d0]
cbmc(+0xa7ad79) [0x563f38c04d79]
cbmc(+0x1eb218) [0x563f38375218]
cbmc(+0x689d16) [0x563f38813d16]
cbmc(+0x3418b2) [0x563f384cb8b2]
cbmc(+0x35bb6c) [0x563f384e5b6c]
cbmc(+0x1f25f4) [0x563f3837c5f4]
cbmc(+0x1f1aca) [0x563f3837baca]
cbmc(+0x1e92af) [0x563f383732af]
cbmc(+0x1d5359) [0x563f3835f359]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7fec6853e0b3]
cbmc(+0x1eac2e) [0x563f38374c2e]


--- end invariant violation report ---
Aborted (core dumped)

Similar to above, removing --z3 or --json-ui makes the crash go away.