Issues

• SMT2 backend truncates shift distances wider than the shifted operand, including integer constants

  diffblue/cbmc#9374 · Filter by author JeroenRobben opened on Oct 28, 2026

• Float division with a subnormal dividend is rounded incorrectly (CBMC proves a wrong quotient)

  diffblue/cbmc#9373 · Filter by author JeroenRobben opened on Oct 28, 2026

• SMT2 backend with FPA but without datatypes emits ill-typed SMT-LIB for arrays of structs with a float member

  diffblue/cbmc#9372 · Filter by author JeroenRobben opened on Oct 28, 2026

• SMT2 backend aborts or emits invalid SMT-LIB for several arithmetic conversions

  diffblue/cbmc#9371 · Filter by author JeroenRobben opened on Oct 28, 2026

• SMT2 backends: crashes and solver errors on quantified OBJECT_SIZE, flexible array members, arrays in structs (Yices) and compound literals in quantifiers

  diffblue/cbmc#9370 · Filter by author JeroenRobben opened on Oct 28, 2026

• SMT2 backend emits an ill-sorted extract when casting a wider integer to a pointer

  diffblue/cbmc#9369 · Filter by author JeroenRobben opened on Oct 28, 2026

• popcount/clz/ctz/ffs lowerings are wrong for signed operands whose width is not a power of two

  diffblue/cbmc#9368 · Filter by author JeroenRobben opened on Oct 28, 2026

• SMT2 backend: extractbit with a non-constant index casts the index to the source type

  diffblue/cbmc#9367 · Filter by author JeroenRobben opened on Oct 28, 2026

• SMT2 backend ignores the lower bound when casting between integer range types

  diffblue/cbmc#9366 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_convt: hoisted array_of / array literal definitions escape let and quantifier binders, and the array_of forall captures a symbol named i

  diffblue/cbmc#9365 · Filter by author JeroenRobben opened on Oct 28, 2026

• Incremental SMT2 backend: empty struct members are 8 bits wide in struct values but 0 bits in member offsets

  diffblue/cbmc#9364 · Filter by author JeroenRobben opened on Oct 28, 2026

• Incremental SMT2 backend computes wrong address for &a[i][j] (outer index scaled by inner element size)

  diffblue/cbmc#9363 · Filter by author JeroenRobben opened on Oct 28, 2026

• Incremental SMT2 backend extends shift operands by type signedness instead of shift kind when widths differ

  diffblue/cbmc#9362 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_solver aborts on: assert after check-sat, fp.to_sbv/fp.to_ubv with non-RTZ rounding, out-of-range extract

  diffblue/cbmc#9361 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_solver: get-model prints quoted symbols unquoted; n-ary bvxnor/bvnand/bvnor accepted with non-standard semantics

  diffblue/cbmc#9360 · Filter by author JeroenRobben opened on Oct 28, 2026

• float_utils normalisation shift cannot shift by width-1 when the width is 2^k+1

  diffblue/cbmc#9359 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2 front end: bv_division (bvudiv/bvsdiv) captures a user symbol named "divisor", and bvsdiv by zero ignores the dividend's sign

  diffblue/cbmc#9358 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_solver: expanding define-fun applications is not capture-avoiding

  diffblue/cbmc#9357 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_solver silently ignores push, pop, reset-assertions and reset

  diffblue/cbmc#9356 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_solver: array disequality is not enforced (no extensionality); returned model violates the assertion

  diffblue/cbmc#9355 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_solver: = / distinct on FloatingPoint compare bit patterns, so two NaNs are unequal

  diffblue/cbmc#9354 · Filter by author JeroenRobben opened on Oct 28, 2026

• smt2_solver answers sat after dropping assertions it could not parse or encode

  diffblue/cbmc#9353 · Filter by author JeroenRobben opened on Oct 28, 2026

• C library model: GCC builtins without a model (__builtin_tgmath, __builtin_sqrt/floor/fmod/pow/fma, __builtin_parity*, __builtin_clrsb*, ...) return unconstrained values

  diffblue/cbmc#9352 · Filter by author JeroenRobben opened on Oct 28, 2026

• SAT backend treats constant shift and rotate distances above INT_MAX as zero

  diffblue/cbmc#9351 · Filter by author JeroenRobben opened on Oct 28, 2026

• cbmc --cvc5 reports VERIFICATION ERROR on any memset and on long double: cvc5 is started without --arrays-exp / --fp-exp

  diffblue/cbmc#9350 · Filter by author JeroenRobben opened on Oct 28, 2026