Bitwuzla reports error on simple function verification

[rod-chapman]

CBMC version: 6.0.1 (HEAD of develop branch, 16th July 2024)
Operating system: macOS
Exact command line resulting in the issue: See below
What behaviour did you expect: success
What happened instead: error from Bitwuzla

Verification of the "zero_slice" function here:
https://github.com/rod-chapman/cbmc-examples/tree/main/arrays

works fine with Z3, but causes a weird error from Bitwuzla 0.5.0

To reproduce - clone and pull the repo above, then

cd arrays
goto-cc --function zero_slice_harness -DCBMC -o ar.goto ar.c
goto-instrument --dfcc zero_slice_harness --apply-loop-contracts --enforce-contract zero_slice  ar.goto ar_contracts.goto
cbmc --verbosity 6 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --smt2 ar_contracts.goto

so far so good - it all works fine with Z3. But try the final step with Bitwuzla 0.5.0:

cbmc --verbosity 6 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --bitwuzla ar_contracts.goto

and it fails with many "ERROR" lines on the output.

To see a bit more details, we can capture the SMT2 output, thus:

cbmc --verbosity 6 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --bitwuzla --outfile zero_slice_bitwuzla.smt2 --bitwuzla ar_contracts.goto

then

bitwuzla zero_slice_bitwuzla.smt2

yields

[error] zero_slice_bitwuzla.smt2:3409:89: undefined symbol 'lambda'

Line 3409 of that file contains

(define-fun |symex_dynamic::dynamic_object$10#3| () (Array (_ BitVec 64) (_ BitVec 8)) (lambda (($array_comprehension_index_u_a_v1 (_ BitVec 64))) (ite (or (not (bvsge $array_comprehension_index_u_a_v1 (_ bv0 64))) (bvuge $array_comprehension_index_u_a_v1 |__CPROVER_contracts_write_set_havoc_slice::1::car!0@1#2..size|)) (select |symex_dynamic::dynamic_object$10#2| $array_comprehension_index_u_a_v1) (select |__CPROVER_contracts_write_set_havoc_slice::$tmp::tmp_nondet_contents!0@1#1| $array_comprehension_index_u_a_v1))))

Note the appearance of "lambda" in that line - it does not appear anywhere else in the file... so not sure what's going wrong there...

[tautschnig]

It seems that Bitwuzla doesn't actually support lambda expressions. Fixed in #8387. Your example appears to work fine with Bitwuzla with that change in place.