All pull requests

Pull requests

• 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

• Incremental SMT back-end: support extractbit with a constant index

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

  ·
  2

• jbmc-strings/ConstantEvaluationTrim: run the tab and linebreak tests

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

  ·
  2

• DFCC: Add opt-in to force call by contract

  #9465·hanno-becker opened Nov 13, 2026·

  ·

• SMT2: declare datatypes of pointed-to structs after the pointing struct

  #9464·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Library linking: a callee only a model declares is in the goto program

  #9463·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Goto conversion: the floating-point comparison macros are relations

  #9462·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  3

• va_start: the variadic arguments follow the last named parameter

  #9460·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• CodeQL: build with JDK 21

  #9459·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Slicer: ignore GOTO steps over sliced assignments

  #9458·albertwujj opened Nov 12, 2026·6 tasks done·

  ·

• C front-end: decreases clause types and pointer comparisons

  #9457·tautschnig opened Nov 12, 2026Collaborator·2 of 3 tasks·

  ·
  2

• generate-function-body: reuse free-suffix hints when havocking

  #9456·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  3

• Loop contracts file: report bad clauses and loop identifiers instead of crashing

  #9455·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  13

• Symex: warn when arrays of structs or pointers exceed the field-sensitivity limit

  #9454·tautschnig opened Nov 12, 2026Collaborator·3 of 4 tasks·

  ·
  2

• goto_inline: handle arguments of a type that differs from the parameter's

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

  ·
  2

• DFCC: pass the write set where the write set parameter is

  Code Contracts
  #9452·tautschnig opened Nov 12, 2026Collaborator·4 tasks done·

  ·
  9

• DFCC: test that checks inside uncontracted loops are not all suppressed

  #9451·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2