Invariant violation with bitwuzla backend due to ID_infinity

[remi-delmas-3000]

This model fails with CBMC 6.4.1 with the bitwuzla back end cbmc --bitwuzla. The same model works with --z3 .

The problem goes away if I change the declaration of invalid from size_t invalid; to void *invalid;.

#include <stdlib.h>

int main() {
  size_t n;
  __CPROVER_assume(n > 0);
  char *p;
  int success;
  if (success) {
    p = __CPROVER_allocate(n, 0);
  } else {
    size_t invalid; // needed
    p = (void *)invalid; // needed
  }
  __CPROVER_assume(success);
  char nondet[n];
  __CPROVER_array_replace(p, nondet); // needed
  *p; // needed
}

❯ cbmc --bitwuzla infinity.c --outfile instance.smt2
CBMC version 6.4.1 (cbmc-6.4.1-133-ge98ffb332a-dirty) 64-bit x86_64 macos
Type-checking infinity
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Outputting SMTLib formula to file: instance.smt2
Passing problem to SMT2
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: /Users/delmasrd/projects/cbmc/src/solvers/smt2/smt2_conv.cpp:2586 function: convert_expr
Condition: smt2_convt::convert_expr should not be applied to unsupported expression
Reason: false
Backtrace:
0   cbmc                                0x000000010f6b6c4a _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   cbmc                                0x000000010f6b74a8 _Z13get_backtracev + 184
2   cbmc                                0x000000010f0aaa60 _Z29invariant_violated_structuredI34invariant_with_diagnostics_failedtJRNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEES7_EENS1_9enable_ifIXsr3std10is_base_ofI17invariant_failedtT_EE5valueEvE4typeERKS7_SF_iSF_DpOT0_ + 48
3   cbmc                                0x000000010f40c6f4 _Z24report_invariant_failureIJRKNSt3__112basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEEEEvS8_S8_iS6_S6_DpOT_ + 68
4   cbmc                                0x000000010f4911b4 _ZN10smt2_convt12convert_exprERK5exprt + 23908
5   cbmc                                0x000000010f4889c2 _ZN10smt2_convt12find_symbolsERK5exprt + 2722
6   cbmc                                0x000000010f487feb _ZN10smt2_convt12find_symbolsERK5exprt + 203
7   cbmc                                0x000000010f498263 _ZN10smt2_convt24prepare_for_convert_exprERK5exprt + 1267
8   cbmc                                0x000000010f4a8c44 _ZN10smt2_convt6set_toERK5exprtb + 996
9   cbmc                                0x000000010f1feac2 _ZN22symex_target_equationt19convert_assignmentsER19decision_proceduret + 306
10  cbmc                                0x000000010f1fe640 _ZN22symex_target_equationt26convert_without_assertionsER19decision_proceduret + 208
11  cbmc                                0x000000010f2003d3 _ZN22symex_target_equationt7convertER19decision_proceduret + 35
12  cbmc                                0x000000010f0819cb _Z29convert_symex_target_equationR22symex_target_equationtR19decision_proceduretR16message_handlert + 315
13  cbmc                                0x000000010f08312d _Z24prepare_property_deciderRNSt3__13mapI8dstringt14property_infotNS_4lessIS1_EENS_9allocatorINS_4pairIKS1_S2_EEEEEER22symex_target_equationtR28goto_symex_property_decidertR19ui_message_handlert + 413
14  cbmc                                0x000000010f08f66a _ZN25multi_path_symex_checkertclERNSt3__13mapI8dstringt14property_infotNS0_4lessIS2_EENS0_9allocatorINS0_4pairIKS2_S3_EEEEEE + 234
15  cbmc                                0x000000010f077408 _ZN46stop_on_fail_verifier_with_fault_localizationtI25multi_path_symex_checkertEclEv + 40
16  cbmc                                0x000000010f075f55 _ZN19cbmc_parse_optionst4doitEv + 3125
17  cbmc                                0x000000010f6e888f _ZN19parse_options_baset4mainEv + 143
18  cbmc                                0x000000010f06a618 main + 40
19  dyld                                0x00007ff8080852cd start + 1805

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

--- end invariant violation report ---

The infinity term occurs for the array_size expression at this line

cbmc/src/solvers/smt2/smt2_conv.cpp

Line 5189 in 97c8624

convert_expr(array_size);

due to the combination of

    size_t invalid; // needed
    p = (void *)invalid; // needed

and

  char nondet[n];
  __CPROVER_array_replace(p, nondet); // needed