Crash during SMT translation of `NULL` pointers

[SaswatPadhi]

CBMC version: 99f1a2e

Operating system: Mac OS 10.15.7

Test case:

#include <string.h>

void main()
{
    char *data = NULL;
    memset(data, 0, 8);
    memset(data, 0, 8);
}

Exact command line resulting in the issue:

$ cbmc --z3 test.c

What behaviour did you expect:

CBMC would report a verification failure.

What happened instead:

CBMC crashed during SMT translation:

invariant violation report

--- begin invariant violation report ---
Invariant check failed
File: smt2/smt2_conv.cpp:4750 function: convert_type
Condition: Precondition
Reason: false
Backtrace:
0   cbmc                                0x0000000102f6ea7a _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x0000000102f6f002 _Z13get_backtracev + 210
2   cbmc                                0x0000000102f94660 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 48
3   cbmc                                0x0000000102f9ab14 _Z24report_invariant_failureIJNSt3__112basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEEEEvRKS6_S8_iS6_S6_DpOT_ + 68
4   cbmc                                0x0000000102f0d78b _ZN10smt2_convt12convert_typeERK5typet + 3067
5   cbmc                                0x0000000102f14db0 _ZN10smt2_convt12find_symbolsERK5exprt + 3808
6   cbmc                                0x0000000102effa3f _ZN10smt2_convt24prepare_for_convert_exprERK5exprt + 47
7   cbmc                                0x0000000102f133bb _ZN10smt2_convt6set_toERK5exprtb + 763
8   cbmc                                0x0000000102cecb25 _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 261
9   cbmc                                0x0000000102cec785 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 117
10  cbmc                                0x0000000102cedf33 _ZN22symex_target_equationt7convertER19decision_proceduret + 35
11  cbmc                                0x0000000102b8c316 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 342
12  cbmc                                0x0000000102b8e229 _Z24prepare_property_deciderRNSt3__113unordered_mapI8dstringt14property_infotNS_4hashIS1_EENS_8equal_toIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 441
13  cbmc                                0x0000000102b96007 _ZN25multi_path_symex_checkertclERNSt3__113unordered_mapI8dstringt14property_infotNS0_4hashIS2_EENS0_8equal_toIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 247
14  cbmc                                0x0000000103017ad3 _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 51
15  cbmc                                0x000000010300f879 _ZN19cbmc_parse_optionst4doitEv + 4409
16  cbmc                                0x0000000102f89538 _ZN19parse_options_baset4mainEv + 136
17  cbmc                                0x000000010300ac38 main + 40
18  libdyld.dylib                       0x00007fff6a4becc9 start + 1

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
unsupported type: empty
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---

Additional information:

The variable need not be NULL explicitly, but if it could be set to NULL in any branch, it still leads to a crash:

// crash
#include <string.h>

void main()
{
    char *data = nondet() ? NULL : malloc(8);
    memset(data, 0, 8);
    memset(data, 0, 8);
}

But the following program (where data cannot be NULL) does not lead to a crash during translation:

// no crash
#include <stdlib.h>
#include <string.h>

void main()
{
    char *data = nondet() ? malloc(16) : malloc(8);
    memset(data, 0, 8);
    memset(data, 0, 8);
}

Also, a single memset invocation does not lead to a crash and works as expected:

// no crash
#include <string.h>

void main()
{
    char *data = NULL;
    memset(data, 0, 8);
}

[SaswatPadhi]

The issue appears to be with the encoding of NULL pointers in general.

$ cat test_2.c
#include <stdlib.h>

void main()
{
    assert(NULL != (NULL + 1));
}

$ cbmc test_2.c
[... VERIFICATION SUCCESSFUL ...]

$ cbmc --smt2 test_2.c
[... crash in convert_plus ...]