All pull requests

Pull requests

• Fix conversion of integers of width 2^k+1 to floating-point

  #9493·tautschnig opened Nov 14, 2026Collaborator·3 tasks done·

  ·
  1

• Incremental SMT2: floating-point values are bit patterns

  #9492·tautschnig opened Nov 14, 2026Collaborator·3 tasks done·

  ·
  1

• Incremental SMT2: preserve sharing in the encoding of floats

  dependent - do not merge
  #9491·tautschnig opened Nov 14, 2026Collaborator·3 of 4 tasks·

  ·

• Raise the minimum macOS deployment target to 11.0

  #9490·mkannwischer opened Nov 14, 2026Contributor·3 of 7 tasks·

  ·
  1

  1

• Incremental SMT2: support the bit-vector encoding of float conversions

  dependent - do not merge
  #9488·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  1

• Fix reconstruction of arrays with zero-width elements

  #9487·Tiramisu-Cake opened Nov 13, 2026·7 tasks done·

  ·
  1

• Symex: do not convert field-sensitive declared objects as a whole

  #9486·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• Symex: rename enclosing object types in field SSA expressions

  #9485·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• SMT2 output: declare logic ALL when using the FPA theory

  #9484·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• Field sensitivity: project members of field-sensitive structs

  #9483·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• Value sets: find a field-sensitive member read through a member expression

  #9482·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• remove_complex: lower the parameter and return types of code types

  #9481·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• Print __CPROVER_fma before its rounding mode is added; dump-c includes math.h

  #9480·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• C library: models of wcslen, wmem* and wcsto{l,ul,ll,ull}

  #9479·tautschnig opened Nov 13, 2026Collaborator·4 tasks done·

  ·
  1

• goto_check_c: no guards from constant operands of ||, && and ?:

  #9478·tautschnig opened Nov 13, 2026Collaborator·3 of 4 tasks·

  ·
  2

• Field sensitivity: read a union through its widest member at any offset

  #9477·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• smt2: convert between mathematical integers and bit-vectors or floats

  #9476·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• smt2: flatten non-constant floats to bit-vectors with the FPA theory

  #9475·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• Add --isolate-properties: decide each property in its own solver call

  #9474·tautschnig opened Nov 13, 2026Collaborator·4 of 6 tasks·

  ·
  2

• value_set_dereference: no byte model for types without a byte layout

  #9473·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• util: amortise symbol_table_baset::next_unused_suffix

  #9472·tautschnig opened Nov 13, 2026Collaborator·5 tasks done·

  ·
  2

• boolbv_get: do not fail on values that the encoding does not represent

  #9471·tautschnig opened Nov 13, 2026Collaborator·2 of 3 tasks·

  ·
  2

• full_slicer: do not remove ASSUME false

  #9470·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2

• smt2: lower empty_string and decimal of_int to SMT-LIB

  dependent - do not merge
  #9469·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  1

• ieee_float, floatbv: keep NaN payloads, and make the default NaN quiet

  #9468·tautschnig opened Nov 13, 2026Collaborator·3 tasks done·

  ·
  2