Issues

• False data race reported on the unevaluated operand of ?:

  ftsrg/theta#609 · Filter by author leventeBajczi opened on Oct 3, 2026

• Nondeterministic result on identical input and flags (25 s / 129 s / timeout)

  ftsrg/theta#610 · Filter by author leventeBajczi opened on Oct 3, 2026

• FpLitExpr.isPositiveZero/isNegativeZero test the sign bit the wrong way round (wrong verdicts on ±0.0)

  bug
  ftsrg/theta#606 · Filter by author leventeBajczi opened on Sep 30, 2026

• SPOR misses a data race whose array index is read through a pointer (wrong no-data-race true)

  xcfa
  ftsrg/theta#605 · Filter by author leventeBajczi opened on Sep 30, 2026

• OC PROPAGATOR gives wrong true verdicts on pointer-heavy tasks

  ftsrg/theta#603 · Filter by author leventeBajczi opened on Sep 30, 2026
  

• Bad memory initialization statements for nested structs

  ftsrg/theta#602 · Filter by author csanadtelbisz opened on Sep 30, 2026
  

• Transition invariants: witnesses for termination

  svcomp
  Feature

  ftsrg/theta#600 · Filter by author mondokm opened on Sep 29, 2026
  

• BvLitExpr.urem reads its operands as signed

  bugcore
  ftsrg/theta#597 · Filter by author leventeBajczi opened on Sep 28, 2026

• Aggregate members of malloc'd objects are never allocated (false valid-deref)

  bugxcfa
  ftsrg/theta#596 · Filter by author leventeBajczi opened on Sep 28, 2026

• A redeclaration after a definition drops the variable's initializer

  bugxcfa
  ftsrg/theta#595 · Filter by author leventeBajczi opened on Sep 28, 2026

• Zero-initialised global union with a struct first member reads back non-zero

  bugxcfa
  ftsrg/theta#594 · Filter by author leventeBajczi opened on Sep 28, 2026

• OC misses a lost-update race when the final check has two calls joined by ||

  bugxcfa
  ftsrg/theta#593 · Filter by author leventeBajczi opened on Sep 28, 2026

• Analysis precision leftovers found during triage

  xcfa
  ftsrg/theta#592 · Filter by author leventeBajczi opened on Sep 28, 2026
  1

• checkCopyright/applyCopyright report wrong years in shallow clones

  bug
  ftsrg/theta#591 · Filter by author leventeBajczi opened on Sep 28, 2026

• Solver-layer bugs found during triage

  bugsolver
  ftsrg/theta#590 · Filter by author leventeBajczi opened on Sep 28, 2026
  1

• Frontend, pass and CLI bugs found during triage

  bugxcfa
  ftsrg/theta#589 · Filter by author leventeBajczi opened on Sep 28, 2026
  1

• Wrong verdicts from the __atomic_* builtin model: pointer fetch_add scaling, user-defined atomic_load overridden

  bugsvcomp
  ftsrg/theta#587 · Filter by author leventeBajczi opened on Sep 28, 2026

• Support the remaining atomic builtins: __atomic_test_and_set, __atomic_clear, __atomic_*_lock_free, atomic_flag_*

  svcomp
  ftsrg/theta#586 · Filter by author leventeBajczi opened on Sep 28, 2026

• sizeof of an array type name drops the array declarator

  bugxcfa
  ftsrg/theta#585 · Filter by author leventeBajczi opened on Sep 28, 2026

• --datarace-to-reachability fails in the frontend on programs calling memset

  ftsrg/theta#583 · Filter by author leventeBajczi opened on Sep 27, 2026

• Flat memory encoding issue

  ftsrg/theta#577 · Filter by author csanadtelbisz opened on Sep 22, 2026
  

• Statement expression drops reach_error() (2SB, 4SB)

  ftsrg/theta#575 · Filter by author AdamZsofi opened on Sep 18, 2026
  

• solver-z3 (Z3:new) produces unusable interpolants and crashes; legacy Z3 is unaffected

  ftsrg/theta#573 · Filter by author leventeBajczi opened on Sep 17, 2026

• Mid-object pointer loses its offset across a non-inlined call, causing false valid-deref alarms (31 tasks, -496)

  bugneeds theoretical decisions
  ftsrg/theta#571 · Filter by author leventeBajczi opened on Sep 12, 2026
  2

• OC backend reports Safe on a reachable NULL dereference when the alias graph is non-empty

  bug
  ftsrg/theta#570 · Filter by author leventeBajczi opened on Sep 12, 2026
  1