1 Release published by 1 person

• cbmc-6.5.0

  published Mar 13, 2025

14 Pull requests merged by 6 people

• Refine-arithmetic supports simplifier

  #8619 merged Apr 8, 2025

• Replace conditions in quantified statement expressions

  #8618 merged Apr 6, 2025

• Remove set but not used variables

  #8595 merged Apr 4, 2025

• Remove unused {c,java}_qualifierst::count

  #8583 merged Apr 4, 2025

• Upgrade CVC5 in CI to 1.2.1

  #8585 merged Apr 4, 2025

• Fix filename completion in bash autocompletion

  #8587 merged Apr 4, 2025

• Fix quantifiers with nested statement-expressions

  #8616 merged Apr 4, 2025

• CI: Remove use of Ubuntu 20.04

  #8613 merged Apr 4, 2025

• Use same CMake minimum version in DownloadProject configuration

  #8611 merged Apr 2, 2025

• Fix display of code changes in clang-format CI action

  #8609 merged Mar 26, 2025

• Release CBMC 6.5.0

  #8607 merged Mar 13, 2025

• Handle quantifiers with statement expressions

  #8605 merged Mar 12, 2025

• CONTRACTS: is_fresh now tracks separation at the byte level instead of whole objects

  #8603 merged Mar 11, 2025

• simplify: rewrite bitxnor on booleans to equal

  #8594 merged Mar 11, 2025

1 Pull request opened by 1 person

• Simplify quantified expressions over constants

  #8608 opened Mar 24, 2025

1 Issue closed by 1 person

• Soundness with __CPROVER_r_ok

  #8614 closed Apr 2, 2025

5 Issues opened by 5 people

• Huge SMT file and slow proof for simple array function

  #8617 opened Apr 3, 2025

• CBMC getting stuck when post-processing functions with memmove and non-deterministic sizes

  #8615 opened Apr 2, 2025

• Dump-C appears incompatible with --dfcc

  #8612 opened Apr 2, 2025

• Buggy handling of assignments involving pointer dereference

  #8610 opened Mar 31, 2025

• [Question] Running CBMC on a C file with dynamic linking and/or shared libraries

  #8606 opened Mar 10, 2025

6 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• [Question] Syntax Error with `__CPROVER_loop_invariant` in CBMC 6.4.1 Docker

  #8604 commented on Mar 10, 2025 • 0 new comments

• CBMC does not recognize pointer initializations outside functions

  #8593 commented on Apr 2, 2025 • 0 new comments

• Quantifier instantiation via simplistic E-matching

  #8224 commented on Mar 25, 2025 • 0 new comments

• C++ front-end fixes

  #8275 commented on Apr 4, 2025 • 0 new comments

• Adding large-step encoding for CHCs in CProver (no [required] changes to the solver)

  #8465 commented on Apr 5, 2025 • 0 new comments

• Cleanup type conversions in java_bytecode_parsert::read

  #8584 commented on Apr 4, 2025 • 0 new comments