Printing SMT file with Z3 backend crashes CBMC

[rod-chapman]

Attempt to print out the SMT file generated by the Z3 backend fails with a crash on some functions in the mldsa-native codebase. See this directory, for example:
https://github.com/pq-code-package/mldsa-native/tree/main/proofs/cbmc/poly_invntt_tomont

Using CBMC 6.6.0 in that directory, proof with Bitwuzla:

make goto
cbmc  --bitwuzla --flush --object-bits 9    --conversion-check  --float-overflow-check --nan-check  --pointer-overflow-check    --unsigned-overflow-check gotos/poly_invntt_tomont_harness.goto

works fine. Similarly, proof with Z3:

make goto
cbmc  --smt2 --flush --object-bits 9    --conversion-check  --float-overflow-check --nan-check  --pointer-overflow-check    --unsigned-overflow-check gotos/poly_invntt_tomont_harness.goto

also works fine (but is much faster).

BUT... attempt to print and save the SMT file for Z3:

make goto
cbmc  --smt2 --flush --object-bits 9    --conversion-check  --float-overflow-check --nan-check  --pointer-overflow-check    --unsigned-overflow-check --outfile z.smt2 --smt2 gotos/poly_invntt_tomont_harness.goto

fails with a crash

converting SSA
--- begin invariant violation report ---
Invariant check failed
File: /tmp/nix-build-cbmc-6.6.0.drv-0/source/src/solvers/smt2/smt2_conv.cpp:4780 function: unflatten
Condition: use_as_const
Reason: Precondition
Backtrace:
0   cbmc                                0x00000001006b18d8 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 124
1   cbmc                                0x00000001006b1d9c _Z13get_backtracev + 180
2   cbmc                                0x00000001000b7640 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 68
3   cbmc                                0x00000001000b7554 _ZNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEC1B7v160006IDnEEPKc + 0
4   cbmc                                0x00000001004cc850 _ZN10smt2_convt9unflattenENS_6wheretERK5typetj + 1912
5   cbmc                                0x00000001004cd118 _ZN10smt2_convt6set_toERK5exprtb + 1880
6   cbmc                                0x000000010022c854 _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 272
7   cbmc                                0x000000010022c3f0 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 224
8   cbmc                                0x000000010022ddc4 _ZN22symex_target_equationt7convertER19decision_proceduret + 48
9   cbmc                                0x00000001000cb578 _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 276
10  cbmc                                0x00000001000cceb0 _Z24prepare_property_deciderRNSt3__13mapI8dstringt14property_infotNS_4lessIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 388
11  cbmc                                0x00000001000d76dc _ZN25multi_path_symex_checkertclERNSt3__13mapI8dstringt14property_infotNS0_4lessIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 252
12  cbmc                                0x00000001000c13a4 _ZN46stop_on_fail_verifier_with_fault_localizationtI25multi_path_symex_checkertEclEv + 56
13  cbmc                                0x00000001000bffcc _ZN19cbmc_parse_optionst4doitEv + 2872
14  cbmc                                0x00000001006e2400 _ZN19parse_options_baset4mainEv + 240
15  cbmc                                0x00000001000b6c98 main + 56
16  dyld                                0x000000018c4aab4c start + 6000

This makes debugging and performance testing of proof failures difficult.

[rod-chapman]

Note that the code in questions (smt_conv.cpp) was last modified as part of
#8400
which fixed the generation of SMT for bitwuzla.

[tautschnig]

Note that the above command lines will not actually trigger the same code paths: —smt2 —outfile produces SMT2 for a „generic“ pseudo-solver. Use —z3 —outfile (and perhaps always use —z3 instead of —smt2) to get the same output as is otherwise sent to Z3.

[rod-chapman]

Ah... so

cbmc  --smt2 --flush --object-bits 9    --conversion-check  --float-overflow-check --nan-check  --pointer-overflow-check    --unsigned-overflow-check --outfile z.smt2 gotos/poly_invntt_tomont_harness.goto

produces the crash, but

cbmc  --smt2 --flush --object-bits 9    --conversion-check  --float-overflow-check --nan-check  --pointer-overflow-check    --unsigned-overflow-check --outfile z.smt2 --z3 gotos/poly_invntt_tomont_harness.goto

does not crash. (Note the extra --z3 after --outfile).

[rod-chapman]

Here are instructions to reproduce this issue. I have reproduced this using CBMC 6.6.0 and the wavefront from the simp-combined branch.

First, checkout the main branch of the mlkem-native repo, then

cd proofs/cbmc/polyvec_add

make goto

cbmc --no-array-field-sensitivity --slice-formula --flush --object-bits 8    --conversion-check --float-overflow-check --nan-check  --pointer-overflow-check --unsigned-overflow-check --bitwuzla --outfile b.smt2 --bitwuzla gotos/polyvec_add_harness.goto

bitwuzla b.smt2

results in

[error] b.smt2:970:144: element sort of array and sort of element do not match

That's using bitwuzla 0.7.0, all on macOS.

[tautschnig]

#8670 addresses the issued observed when using Bitwuzla. The original issue of crashing when trying to print the formula should likely be addressed by removing support for any solvers that don't permit as const SMT-LIB syntax. But, also, users should specify the target solver with --outfile to obtain meaningful output.