Invariant violation: simple pointer assignment with --smt2, --enforce-contract, and __CPROVER_is_fresh

[BeamRaceMuppet]

CBMC version: 6.1.1

Using --smt2 together with --enforce-contract to check a simple function contract using __CPROVER_is_fresh with __CPROVER_assigns triggers an internal invariant violation in CBMC. Small reproducer:

void foo(char *p)
__CPROVER_requires(__CPROVER_is_fresh(p, sizeof(*p)))
__CPROVER_assigns(*p)
{
    *p = 'x';
}

Run CBMC like this:

goto-cc foo.c -o foo.goto && goto-instrument --enforce-contract foo foo.goto foo.i.goto && cbmc --smt2 --function foo foo.i.goto

Expected behavior: VERIFICATION SUCCESSFUL.

Observed behavior:

Reading GOTO program from 'foo.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Enforcing contracts
line 9 function __CPROVER_enforce_requires_is_fresh: function 'malloc' is not declared
Adding nondeterministic initialization of static/global variables.
Writing GOTO program to 'foo.i.goto'
CBMC version 6.1.1 (cbmc-6.1.1) 64-bit x86_64 linux
Reading GOTO program from file foo.i.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-malloc> line 11: implicit function declaration 'malloc'
old definition in module <built-in-library> line 9 function __CPROVER_enforce_requires_is_fresh
void * (void)
new definition in module <built-in-library> file <builtin-library-malloc> line 11
void * (__CPROVER_size_t malloc_size)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Running SMT2 QF_AUFBV using Z3
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:2480 function: convert_expr
Condition: smt2_convt::convert_expr should not be applied to unsupported type
Reason: false
Backtrace:
cbmc(+0xa4aa72) [0x5588a5d26a72]
cbmc(+0xa4b7ed) [0x5588a5d277ed]
cbmc(+0x177a29) [0x5588a5453a29]
cbmc(+0x7e8636) [0x5588a5ac4636]
cbmc(+0x7ce561) [0x5588a5aaa561]
cbmc(+0x7e051e) [0x5588a5abc51e]
cbmc(+0x7e0690) [0x5588a5abc690]
cbmc(+0x7ec6cd) [0x5588a5ac86cd]
cbmc(+0x72e44e) [0x5588a5a0a44e]
cbmc(+0x28057b) [0x5588a555c57b]
cbmc(+0x29008d) [0x5588a556c08d]
cbmc(+0x158218) [0x5588a5434218]
cbmc(+0x153b43) [0x5588a542fb43]
cbmc(+0x14aadf) [0x5588a5426adf]
cbmc(+0x138769) [0x5588a5414769]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x7f0f20c071ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x7f0f20c0728b]
cbmc(+0x14c475) [0x5588a5428475]

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
infinity
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
Aborted

Removing --smt2 results in success:

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS

foo.c function foo
[foo.assigns.1] line 6 Check that *p is valid: SUCCESS
[foo.assigns.2] line 8 Check that *p is assignable: SUCCESS
[foo.pointer_dereference.1] line 8 dereference failure: pointer NULL in *p: SUCCESS
[foo.pointer_dereference.2] line 8 dereference failure: pointer invalid in *p: SUCCESS
[foo.pointer_dereference.3] line 8 dereference failure: deallocated dynamic object in *p: SUCCESS
[foo.pointer_dereference.4] line 8 dereference failure: dead object in *p: SUCCESS
[foo.pointer_dereference.5] line 8 dereference failure: pointer outside object bounds in *p: SUCCESS
[foo.pointer_dereference.6] line 8 dereference failure: invalid integer address in *p: SUCCESS

** 0 of 10 failed (1 iterations)
VERIFICATION SUCCESSFUL