SMT generated for Bitwuzla is mal-formed and rejected

[rod-chapman]

An example from the mldsa-native project.

CBMC 7.6.1 generates SMT which is rejected by Bitwuzla 0.7, typically when array types are involved in a C program.

Simplified example program link in next comment.

[rod-chapman]

Example code here:
https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8686

With cbmc 6.7.1 and bitwuzla 0.7 on PATH, I see:

rodchap@f4d4889dcf6d 8686 % make
rm -f *.goto *.smt2
goto-cc --function mld_polyveck_caddq_harness -DCBMC -o q.goto q.c
goto-instrument --dfcc mld_polyveck_caddq_harness --apply-loop-contracts --enforce-contract mld_polyveck_caddq --replace-call-with-contract caddq q.goto q_contracts.goto
Reading GOTO program from 'q.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (arm64)
Adding the cprover_contracts library (arm64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'mld_polyveck_caddq_harness'
Wrapping 'mld_polyveck_caddq' with contract 'mld_polyveck_caddq' in CHECK mode
file q.h line 13 function mld_polyveck_caddq: no body for function '__CPROVER_object_upto'
file q.c line 14 function mld_polyveck_caddq: no body for function 'caddq'
file q.c line 8 function mld_polyveck_caddq: no body for function '__CPROVER_object_upto'
no body for function '__CPROVER_assignable'
Wrapping 'caddq' with contract 'caddq' in REPLACE mode
file p.h line 13 function caddq: no body for function '__CPROVER_object_upto'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 2 targets
Removing unused functions
generate function bodies: No function name matched regex
Updating init function
Setting entry point to mld_polyveck_caddq_harness
Writing GOTO program to 'q_contracts.goto'
cbmc --bounds-check --pointer-check --undefined-shift-check --enum-range-check --pointer-primitive-check --bitwuzla --outfile b.smt2 --bitwuzla q_contracts.goto
CBMC version 6.7.1 (cbmc-6.7.1) 64-bit arm64 macos
Reading GOTO program from file q_contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Outputting SMTLib formula to file: b.smt2
Passing problem to SMT2
converting SSA
Running SMT2
bitwuzla b.smt2
[error] b.smt2:12136:165: element sort of array and sort of element do not match
make: *** [results] Error 1

[rod-chapman]

This problem affects the following functions in mldsa-native:

polyveck_caddq
polyveck_invntt_tomont
polyveck_ntt
polyveck_power2round
polyveck_reduce
polyveck_shiftl
polyveck_sub
polyveck_use_hint
polyvecl_invntt_tomont
polyvecl_ntt
polyvecl_reduce

[rod-chapman]

I have also tried these examples with Bitwuzla 0.8.1 with the same results.

[tautschnig]

I‘d expect #8670 to fix this.

[rod-chapman]

Super - I will build that branch and report results here.