Release Notes of the ESBMC model checker

*** ESBMC v8.3 Release Notes
This release of ESBMC v8.3 substantially expands the Python frontend with broad tuple and set support, comprehensive dataclass conformance, context manager (with/async with) lowering, and new operational models for collections (deque, OrderedDict), random, and time. C/C++ verification gains C++17/20/23 language features (structured bindings, deducing this, C++20 paren aggregate init, class template argument deduction, if consteval, paren aggregate init) and a large batch of new operational models (std::filesystem, std::any, std::variant, std::expected, std::source_location, std::span, std::underlying_type). The release introduces CWE mapping with SARIF output, k-path coverage, violation-witness validation, a rewritten simplifier with reassociation and peephole expansion, and makes Bitwuzla the default SMT solver. Toolchain support is bumped to Clang 22, and interval range analysis (IR-IEEE) is extended with theorem-driven RNA/RDN/RUP/RTZ rounding-mode lifting for ieee_div. Below is a summary of the new features, enhancements, and bug fixes:

* New Features
** Python Frontend
*** Tuple Support
- Inferred tuple element types for bare 'tuple' annotations (#4524).
- Supported tuple slicing t[a:b:c] (#4370).
- Supported tuple + (concat) and * (repeat) (#4369).
- Supported tuple.count() and tuple.index() (#4368, #4101).
- Supported tuple variable index and for-loop on homogeneous tuples (#4367).
- Honoured key= on min() and max() for tuple-of-constants pattern (#4393).
- Supported tuples in all()/any() and rejected unknown args (#4302).
- Supported tuple type aliases and hardened list literal folding (#4165).
*** Set Support
- Added support for set comprehensions (#4371).
- Added support for set.add() and set.discard() (#4365).
- Added issubset / update / symmetric_difference / frozenset (#4392).
- Accepted set and Set-literal iterables in any() / all() (#4362).
*** Dataclass Support
- Added dataclass decorator expansion for the Python frontend (#4155).
- Added dataclass module import infrastructure (#4142).
- Added dataclass public API support and coverage (#4329).
- Extended dataclass conformance support (#4387).
- Supported advanced dataclass flags, derived methods and inheritance (#4197).
- Stabilised dataclass lifecycle semantics (#4178).
- Synthesised __init__ with field(), default_factory and aliased imports (#4167).
- Refactored to extract DataclassMixin from the preprocessor (#4487).
*** Context Managers
- Supported with/async with statements via preprocessor desugaring (#4152).
- Honoured __exit__ True return for context-manager suppression (#4372).
- Documented with/async with support and its limitation.
*** Type Inference and Annotations
- Inferred class type for methods returning self (#4522).
- Supported range aliases and trivial range wrappers (#4521).
- Inferred concrete types for None-initialised class attributes via usage-site scanning (#4162).
- Added support for inline literals and smarter return-type inference (#4130, #4146).
- Supported tuple type aliases and hardened list literal folding (#4165).
- Guarded infer_loop_variable_types against null AnnAssign value (#4512).
*** Imports and Modules
- Scoped the entry-script skip to top-level module load (#4517).
- Resolved transitive imports through intermediate modules (#4511).
- Gracefully skipped unresolvable imports instead of crashing (#4156).
- Embedded the ast2json library and ran mypy as a subprocess (#3790).
*** Dictionary Operations
- Routed dict.copy() to a dict-aware handler (#4358).
- Supported dict.fromkeys() class method (#4124).
- Fixed dict comprehension to evaluate key/value per iteration (#4299).
- Fixed dict-of-class-instance subscript and value-type inference (#4384).
- Fixed dict subscript attribute access and bare-dict value type inference (#4164).
- Fixed dict_eq and added fast paths for tuple-key sizes (#4227).
*** List Operations
- Honoured key= on list.sort() and sorted() on tracked literals (#4395).
- Honoured reverse= on list.sort() and sorted() (#4363).
- Honoured step in list slicing (xs[::2], xs[::-1]) (#4332).
- Supported list method chains on call-returned receivers (#4103).
- Fixed list string handling and promoted list34 coverage (#4097).
- Fixed list * n for variable lists (#4063).
- Preserved container type on subscript assignment (#4073).
- Fixed join(genexp) lowering in recursive scenario (#4141).
*** Built-ins and Higher-Order Functions
- Added all() builtin function support (#3990).
- Honoured default= keyword on min() and max() (#4360).
- Honoured start in sum(iterable, start) (#4359).
- Honoured fill / align / width in f-string format spec (#4374).
- Supported str(obj).__str__ dispatch and f-string member interpolation (#4068).
*** Module Models
- Added deque and OrderedDict to the collections model (#4376).
- Added seed/choice/shuffle/sample to the random model (#4375).
- Added time module model (#4063).
- Fixed builtin time import for sleep regression (#4069).
*** Robustness and Fixes
- Fixed crash on nested attribute assignment (#4115, #4171).
- Coerced struct class instance to pointer for reference-identity (#4116, #4170).
- Flattened detect_and_process_submodules (#4328).
- Tidied operational-model stubs (#4327).
- Fixed PEP8 E275/E501 in transform.py and models/re.py (#4268).
- Fixed PEP 257 docstring violations in frontend models and parser (#4253).
- Fixed pydocstyle documentation violations (#4221).
- Suppressed pylint rules unsafe to rewrite in operational models (#4265).
- Suppressed pylint function-redefined in model stubs (#4228).
- Silenced Codacy pyflakes F821 on operational models (#4256).
- Disabled Pyflakes F821 via .prospector.yaml (#4257).
- Silenced Codacy redefined-builtin on operational models (#4255).
- Pinned parser.py open() encoding and adopted f-strings (#4261).
- Fixed two use-before-assignment bugs flagged by pylint (#4260).
- Tightened chained comparison in int.from_bytes loop (#4263).
- Removed unused variables and added ForwardRef typing stub (#4231).
*** Regression and Testing
- Added rover simulator and additional Python test cases.
- Added test cases for string and mixed types.
- Promoted python/jpl to CORE with --no-unwinding-assertions (#4099).
- Replaced incidental --incremental-bmc with --unwind N in python/ regressions (#4459).

** C/C++ Verification
*** Language Support (C++17/20/23)
- Supported C++17 structured bindings (#4382).
- Handled C++23 explicit object parameter (deducing this) (#4383).
- Skipped implicit object arg for static operator() (#4381).
- Lowered CXXParenListInitExpr (C++20 paren aggregate init) (#4380).
- Supported C++17/20 class template argument deduction (#4389).
- Mapped char8_t builtin to unsigned 8-bit integer (#4378).
- Emitted init-statement of C++17 if/switch (#4379).
- Handled UsingEnumDecl (C++20 'using enum') (#4204).
- Fixed segfault on C++23 'if consteval' (#4196, #4199).
- Supported C++11 inheriting constructors (using Base::Base) (#4280).
- Added cmp_three_way for the C++20 spaceship operator (#4407).
- Synthesised member/base destructor chain in dtor bodies (#4452).
- Wrapped bitfield LHS in ctor member-init list (#4283).
- Supported noexcept value-dep and 3 member-pointer casts (#4288).
- Lazy-registered methods missing in cross-TU class views (#4417).
- Fixed double-adjustment crash on C++20 padded struct members (#4215).
- Fixed switch-case type mismatch for scoped enum conditions (#4217).
*** Multiple Inheritance and Dispatch
- Fixed explicit cast receiver in multiple inheritance (#4449).
- Throw std::bad_cast on dynamic_cast<T&> failure (#4304).
- Routed dynamic_cast through C++-frontend dispatch (#4147).
- Quick fix for dynamic_cast (#4229).
*** Clang 22 Support
- Handled UsingType for clang >= 22 (#4182, #4187).
- Fixed tag-id mismatch in annotate_class_method on Clang 22+ (#4188).
- Guarded NestedNameSpecifier::getAsType on Clang 22 (#4180, #4184).
- Handled Clang 22 record kind for elaborated types (#4144).
*** GCC and C Extensions
- Supported GCC nested functions (#4072).
- Fixed nested-function transform: gated behind flag, fixed name collision and __label__ (#4100).
- Added byte-level __builtin_bit_cast and fixed list_reference-3 typo (#4411).
- Supported C verification complex type (#4133).
- Supported UserDefinedLiteral node (#4105).
- Fixed value-init crash for derived struct with class base (#4237, #4238).
- Fixed aggregate-init crash for derived struct with bitfield base (#4232, #4233).
- Fixed mk_eq crash on switch with fall-through enum cases (#4234, #4235).
- Fixed index on non-array struct base (#4333).
- Fixed crash on range-based for over 2D array of struct (#4334).
*** Operational Models (C++17/20/23 standard library)
- Added minimal C++17 <filesystem> (#4404).
- Added minimal C++17 <any> (#4391).
- Added minimal C++17 <variant> (#4390).
- Added C++23 <expected> (#4388).
- Added minimal C++20 <source_location> (#4385).
- Added std::span and complete std::type_traits (#4194).
- Added std::underlying_type and underlying_type_t (#4213).
- Added bundled <optional> and <chrono> shims (#4246).
- Added std::clamp to bundled <algorithm> (#4278).
- Added std::chrono::duration::max/min/zero static members (#4277).
- Added std::tuple as a literal type for constexpr arrays (#4276).
- Added const begin()/end() overloads to std::list (#4451).
- Exposed C library names in std:: from <cstdlib> (#4453).
- Exposed float_t and double_t in std via <cmath> (#4287).
- Made std::array accessors constexpr (#4269, #4274).
- Made bundled std::array an aggregate (#4243, #4244).
- Used angle-bracket include for <array> in bundled <span> (#4279).
- Bundled <span> must transitively include <bit> (#4249).
- Bundled <bit> bit_cast<T*> must accept const From (#4250).
- Fixed std::bit_cast<T*> aliasing for symex (#4191, #4192).
- Added state-reset destructors to stack-backed OM containers (#3983, #4172).
- Fixed multiset::insert return type (#4472).
- Fixed find_first_of / find_first_not_of / rfind overloads (#4421).
- Fixed std::string::find_last_of overloads (#4413).
- Fixed sstream operator<< for char and floating-point (#4414).
- Propagated it_str through string iterator copies; NUL temp in append<T> (#4415).
- Fixed <algorithm> heap/sort/partition operations and 6 KNOWNBUG tests (#4409).
- Zero-init class globals and tightened alloca-name match (4 KNOWNBUG) (#4410).
- Enabled two stream/string KNOWNBUG regressions (#4412).
- Enabled gcc-template-tests/pretty1 (Clang __PRETTY_FUNCTION__ form) (#4445).
- Bumped ch16_3 unwind so strchr terminates (#4454).
- Bounded N in cpp_sum_class so k-induction can discharge it (#4450).
- Stopped forcing T() into uninitialized vector slots (#4285).
- Added __ESBMC_HIDE to __VERIFIER_nondet_memory.
*** Function Contracts
- Fixed __ESBMC_is_fresh codegen for the bare-pointer form (#4212).
- Fixed --enforce-contract '*' --function skipping pointer-param allocation (#4075).
*** Concurrency
- Added support for pthread_cancel and the cancellation API (#4138).
- Enabled atomicity-check and interval-symex-guard goto-programs tests (#4059).
- Emitted ATOMIC_BEGIN/END without migrating an empty codet (#4189).

** Solidity Frontend
- Comprehensive Solidity frontend refactoring and implementation (#4236).
- Reclassified constructor_4 regression from THOROUGH to CORE (#4122).
- Addressed Codacy perf findings in Solidity grammar and array_conv (#4323).

** Verification Features
*** CWE Mapping and SARIF Output
- Mapped property violations to CWE ids and added SARIF output (#4488).
- Extended --uninitialised-vars-check to scalar arrays (CWE-457) (#4507).
- Detected uninitialised local scalar reads as CWE-457 (#4501).
- Mapped deadlock-check assertions to CWE-833 (#4499).
- Moved CWE mapping into the Hugo website (#4500).
*** Coverage
- Added --k-path-coverage Phase 1 (issue #4325) (#4330).
- Added k-path spanning-set scoring (#4335 PR1) (#4340).
- Documented --k-path-coverage on the website (#4339).
- Documented --k-path-coverage --generate-ctest-testcase (#4418).
- Documented all coverage modes and fixed the assertion-coverage example (#4457).
- Skipped ASSUME in condition coverage (#4291, #4292).
- Added STL coverage tests for vector/map/set (#4336).
- Aligned nondet_long/ulong with frontend declarations in ctestgen (#4316).
- Emitted portable, round-trip-safe FP literals in CTest cases (#4306).
- Updated deduplication algorithm for ctestcase generation (#4160).
- Silenced cppcheck unusedLabel on __ESBMC_HIDE markers (#4322).
*** Witness
- Added violation witness validation (#4505).
- Added a preprocessor to enable clang to parse the c_expression (#4239).
- Rendered struct fields and floats unambiguously (#4320).
- Enumerated violating inputs per property with --all-witnesses (#4310).
- Moved --all-witnesses/--max-witnesses to the Witness help group (#4324).
- Added special treatment for branching waypoints (#4102).
- Enabled assumption in YAML-based witness waypoint (#4066).
*** Interval Range Analysis (IR-IEEE)
- Added theorem-driven RNA interval lifting for ieee_div (#4062).
- Added theorem-driven RUP interval lifting for ieee_div (#4094).
- Added theorem-driven RDN interval lifting for ieee_div (#4096).
- Added theorem-driven RTZ interval lifting for ieee_div (#4104).
- Fixed isinf/isfinite semantics under --ir-ieee encoding (#4202).
- Demoted noisy float conversion log to debug (#4205).
- Fixed constant_floatbv encoding in int_encoding mode (#4140).
*** Overflow Checking
- Flagged negative shift distance under --overflow-check (#4242).
- Fixed signed shl checks for C++20 [expr.shift]/2 (#4241).
- Skipped C++20 signed shl claim only for non-negative E1 (#4211).
- Don't flag signed left-shift wrap under C++20+ (#4203), with subsequent revert/refinement (#4208).
*** Simplifier
- Simplifier rewrite, reassociation, and peephole expansion (#4282).
*** Symbolic Execution and GOTO
- Preserved __noreturn semantics of __assert_fail under --no-assertions (#4442).
- Modelled missing args on function-pointer calls as nondet (#4289).
- Collapsed phi_function rhs merge into if/else-if/else (#4254).
- Split builtin_functions.cpp into focused files (#4166).
- Removed dead code in builtin_functions/ (codecov cleanup) (#4168).
- Fixed copy_count simplify and added regression tests for builtin_functions (#4169).
- Fixed printf_formatter missing hex/octal specifiers and length modifiers (#4121).
- Fixed malloc with negative size causing vacuous verification (#4114).
- Fixed multi-property missing assertion results in inductive step (#4060).
- Ported goto_inlinet to native irep2 (#4177).
- Ported goto_coverage condition helpers to native irep2 (#4181).
- Ported assign_params_as_non_det to native irep2 (#4176).
- Drained legacy irep from race-detection module (#4175); subsequently reverted (#4259).
*** Pointer Analysis
- Honoured mode.unaligned in check_pointer_alignment (#4273).
- Fixed zero-sized type-pun through struct member (#4113).
- Fixed big-endian byte access into struct via dyn offset (#4108).
*** SMT Backend
- Made Bitwuzla the default SMT solver (#4131).
- Updated supported solvers and features based on CVC5 enhancements (#4161).
- Removed orphaned mk_bvnand / mk_bvnor across all backends (#4465).
- Fixed zero-width struct members in bitcast/byte ops (#4173).
- Fixed crash in byte update when source and update widths are equal (#4111).
- Fixed union array member access to respect endianness (#4112).
- Fixed int-to-ptr cast inconsistency (issue #1539) (#4125).
- Argv model: assume non-null entries per C11 §5.1.2.2.1 (experimental) (#4067).
*** IRep2 and Internals
- Removed dead bitnand2t / bitnor2t expression kinds (#4464).
- Removed dead code_init2t expression kind (#4463).
- Removed unused bvnxor / bitnxor irep (#4286).
- Removed unused cmt_lvalue exprt attribute (#4120).
- Replaced unsigned with size_t for get_num_sub_exprs/get_sub_expr (#4074).
- Lock-free reads for the string interning pool (#4485).
- Replaced C-style casts in bigint and migrated (#4326).
- Replaced C-style casts with explicit C++ casts (#4222).
- Replaced string::find()==0 with starts_with() (#4225).
- Preferred prefix ++/-- for iterators (#4224, #4258, #4266).
- Reduced variable scope in goto_coverage, smt_casts, smt_byteops, solidity_convert (#4223).
- Fixed conditions that are always true or false (Cppcheck) (#4226).
- Tolerated nil sub-operands in base_type(expr2tc&) (#4095).
- Banner and help text print to stdout (#4153).
- Refactored color output logic, reorganised CLI options (carried over from v8.2 polishing).

** Build System
- Respected ENABLE_<solver>=OFF when $HOME/<solver> exists (#4470).
- Enabled cmakelint and fixed lint issues (#4469).
- Slimmed macOS and Windows PR suites (#4461).
- Capped regression timeout and moved long-running tests to disabled/ (#4186).
- Updated Windows LLVM (#4301).
- Bumped pytest to >=9.0.3 (CVE-2025-71176) (#4157).
- Bumped pygments from 2.19.2 to 2.20.0 (#3935).
- Removed Claude code review workflow (#4307).
- Added Claude Code GitHub Workflow (#4185).
- Added query-based filtering to check_python_tests.sh with ignored_dirs preserved (#4174).
- Removed 33 byte-identical duplicate regression tests (#4462).
- Replaced incidental --incremental-bmc with --unwind N (esbmc/) (#4456).
- Updated .gitignore to include build directory pattern.
- Refactored GitHub Actions workflow for coverage upload.
- CI: squash commits now resubmit merged coverage (#4109).
- Added script to extract SV-COMP scores every year (#4110).
- Reformatted clang headers transform.py to 4-space indent (#4262).
- Added esbmc-verifier and creduce-reducer agents.

** Documentation
- Refreshed SV-COMP history graph quarterly (#4154, #4158, #4275, #4303, #4419, #4478, #4483, #4498).
- Added SV-COMP history graph on README/website with quarterly auto-refresh (#4123).
- Rewrote src/solvers README as a developer extension guide (#4471).
- Added README for src/irep2 (#4458).
- Added IRep2 stub page to the theory section (#4468).
- Added SMT formula generation page to the theory section.
- Added SSA Documentation update for the ESBMC website (#4132).
- Streamlined the build guide: quick start vs complete build.
- Updated Python docs: usage, limitations, random model, supported features.
- Reconciled Python limitations doc with current behaviour (#4297).
- Updated Python supported-features with missing constructs and modules.
- Fixed website 404s on Python docs links with mixed-case filenames.
- Fixed doc TOC: stopped nesting all sections under Quantifiers (#4321).
- Consolidated the esbmc-verifier agent description in CLAUDE.md (#4308).
- Added an Available Subagents section and AGENTS.md note (#4298).
- Fixed Zulip link in README.md (#4128, #4148).
- Removed an open parenthesis in the documentation (#4127).
- Updated funding agencies and refined wording in README.
- Fixed build-esbmc-mac.sh description: solvers are optional, Bitwuzla also offered.
- Removed outdated Python frontend disclaimer from the building guide.
- Updated competition statistics in stats-30s.txt, stats-100s, and stats-600s.txt.


*** ESBMC v8.2 Release Notes
This release of ESBMC v8.2 introduces comprehensive complex number support in the Python frontend along with initial generator support and new models for collections.Counter, heapq, and collections.defaultdict. The release adds a theorem-driven interval range analysis (IR-IEEE, formerly IR-RA) covering all IEEE-754 rounding modes for addition, subtraction, multiplication, and division, enables interval-based guard and assertion pruning in symbolic execution, and upgrades Bitwuzla to 0.9.0 with quantifier support. C/C++ verification gains multiple-inheritance virtual dispatch fixes, expanded unique_ptr and function contract support, and a YAML witness parser. Below is a summary of the new features, enhancements, and bug fixes:

* New Features
** Python Frontend
*** Complex Numbers
- Added initial complex number support with type infrastructure, parsing, and type inference (#3705, #3727).
- Completed complex number arithmetic, built-ins, comparisons, and edge coverage (#3732).
- Strengthened complex guards for math and added edge regressions (#3740).
- Completed complex/cmath support, hardened math guards, and fixed large-int complex crash (#3762).
- Added nondet_complex, pow budget, isinstance, str/repr support (#4000).
- Fixed soundness issues, added type promotion and caching for complex numbers (#3947).
- Extracted dedicated complex_handler class and utilities (#3970, #3984).
- Centralized complex attribute access (.real, .imag, .conjugate()) in a dedicated handler (#3986).
- Optimized complex lowering and import symbol resolution caches (#3787).
- Fixed segfault on complex cmath inverse operations (#3774).
- Fixed -Wunused-parameter in handle_complex_to_str (#4058).
*** Generators
- Added initial generator support with stateful next() handling and StopIteration semantics (#3704).
- Fixed crash on recursive generator functions (#3821).
- Fixed spurious counterexample for nested generator functions (#3867).
- Fixed spurious counterexample for recursive generators with type-erased elements (#3870).
- Added any() support with generator expressions (#3706).
*** Collections Module
- Added model for collections.Counter (#3875).
- Added model for heapq (#3998).
- Added initial support for collections.defaultdict (#3845).
*** Dictionary Enhancements
- Implemented dict.update() semantics and dict.update(other_dict) support (#3661, #3914).
- Added initial support for dict.setdefault() (#3662).
- Added support for dict instance attributes (#3872).
- Added dictionary comprehensions (#3918).
- Added support for item in d.items() yielding tuples instead of keys (#3814).
- Fixed dict.get() without default incorrectly failing `is None` check (#3695).
- Fixed dict.get() crash when comparing string values (#3715).
- Fixed dict.pop() verification failure (#3785).
- Fixed dict.popitem() crash on tuple unpacking (#3791).
- Fixed crash on list(d.items()) (#3810).
- Fixed set(d.items()) == {(k,v),...} always failing (#3700).
- Fixed dict[key]() with lambda values incorrectly raising TypeError (#3691).
- Fixed try/except KeyError not catching dict missing-key access (#3718).
- Fixed dereference failure when iterating dict with heterogeneous keys (#3723).
- Fixed Z3 crash and nested dict retrieval for unparameterized dict (#3656).
- Fixed isinstance(None, ...) and dict iteration for nondet collections (#4013).
- Fixed nondet_dict and nondet_list failing to generate sets with multiple elements (#3485).
*** List Operations
- Added list lexicographic ordering operators Lt/LtE/Gt/GtE (#3835).
- Added support for starred unpacking from list variables (#3848).
- Added support for typed list instance attributes in class methods (#3833).
- Added sum() on lists (#3669).
- Avoided copying list payloads in pop() (#4038).
- Fixed pop() on bin expressions and list.extend() with function call arguments (#3688).
- Fixed crash when calling pop()/list methods on nested list subscripts (#3668, #3670).
- Fixed crash on chained list OOB access (#3764).
- Fixed list repetition crash for variable list operands (#3681).
- Fixed list comprehension with multiple for-generators (#3698).
- Fixed list conditions in while loops and conditional expressions (#3883, #4019).
- Fixed list operands in boolean expressions (#3923).
- Fixed sorted(key=lambda x: x[i]) lowering (#4016).
- Fixed unsupported comparison between pointer-backed and non-pointer values when returning list from function (#3699).
- Hardened list/dict reassignment handling (#3676).
- Improved dynamic method fallback and list object storage for jpl_1 (#4042).
*** Type Inference and Annotations
- Added support for typing.NewType and simple type aliases (#4051).
- Handled TypeVar aliases from typing (#3943).
- Allowed unannotated parameters by defaulting to Any (#3721).
- Fixed list type inference for slices (#3937).
- Fixed nested attribute chained method call typing (#4023).
- Fixed class constructor type resolution and supported reflected dunder operators (#3997).
- Fixed annotation type mismatch when function returns str (#3773, #3776).
- Fixed None return path not detected with explicit return annotation (#3770).
- Fixed false positive AttributeError due to loss of parameter type information (#3859).
- Fixed Any arithmetic in Python frontend (#4006).
- Handled short-circuit in boolean conditions (#3888).
- Cast any_type (void*) to integer for arithmetic and ordering ops (#3839).
- Cast integer operands before binary expressions (#4036).
*** Class and Object Support
- Added support for global variable lookup from class methods (#3852).
- Added support for nested attribute chain resolution for non-self base objects (#3834).
- Added support for instance attribute shadowing when set via function parameter (#3828).
- Added support for chained tuple unpacking (#3830).
- Fixed crash on super().__init__() calls (#3687).
- Fixed super().method() crash with return type annotations (#3842).
- Fixed method calls on temporary instances A().f(args) (#3680).
- Fixed annotation crash for A().f() with explicit return type (#3684).
- Fixed crash when calling bound method stored in variable (#3746).
- Fixed crash on nested attribute method call returning string (#3768).
- Fixed crash on chained method calls B().g().f() (#3780).
- Fixed crash on polymorphic calls with different subclass args (#3801).
- Fixed global variable resolution in class methods (#3829).
- Fixed object aliasing: pass mutated class params by pointer (#3734).
- Fixed crash for del on object attributes (#3731).
- Fixed attribute access on Optional forward-reference fields (#3739).
- Added typed attribute-error fallback and dedicated function-call cache hardening (#3878).
*** String Operations
- Refactored string call handling and tightened string method validation (#3909).
- Fixed isspace() segfault and refactored string handling (#3674).
- Fixed crash on nested Unicode encode/decode method chains (#3689).
- Fixed false counterexample for string truthiness and char* indexing (#3917).
- Cleared stale input-len mapping on variable reassignment (#3738).
- Added regression for len(input()) SMT timeout (#3755).
*** Numeric Operations
- Added int.to_bytes() support (#3976).
- Fixed float() on integer expressions causing SMT sort mismatch (#3882).
- Fixed unsound ** operator when exponent is non-constant or float (#3817).
- Supported min()/max() with N >= 2 direct arguments (#3850).
- Fixed min/max crash on unsignedbv/signedbv type mismatch (#3759).
- Fixed crash on max()/min() with mixed int/float lists (#3789).
- Fixed false counterexample for math.sqrt() with constant arguments (#3675).
- Optimized math dispatch/power paths and strengthened cache/typing robustness (#3902).
- Fixed range.__iter__() reported as unsupported (#3753).
*** Lambda and Higher-Order Functions
- Fixed crash for higher-order lambdas (#3725).
- Fixed crash on lambda ternary with None branch (#3798).
- Fixed function alias as default parameter (#3708).
- Fixed indirect higher-order call (#4018).
- Fixed polymorphic call-site specialization (#4030).
*** Iterators and Subscripts
- Added support for reversed(range(...)) in for loops (#3820).
- Resolved subscript via __getitem__/__setitem__ (#3745).
- Resolved tuple subscripts via __getitem__/__setitem__ (#3861).
- Supported __bool__ in conditionals and ternary expressions (#3847, #3857).
- Raised TypeError on tuple item assignment (#3749).
*** Imports
- Supported imports inside function bodies (#3832).
- Improved function name resolution (#3948).
*** Built-ins and Miscellaneous
- Added type() built-in support (#3903).
- Evaluated print() arguments in GOTO to preserve checks (#4001).
- Added support for global variable lookup and initial support for chained assignment (#3840).
- Fixed nested unpacking assignment preprocessing (#3989).
- Fixed github_2012 conversion path (#4020).
*** Regression and Testing
- Added humaneval and quixbugs buggy test suites (#3748, #3905).
- Moved frontend Python tests from tests/ to unit/python-frontend (#3802).

** C/C++ Verification
*** Language Support
- Added __builtin_va_copy handler to eliminate no-body warning (#4057).
- Added support for CXXNoexceptExpr conversion (#4055).
- Handled AtomicToNonAtomic and NonAtomicToAtomic casts (#3949).
- Prepared for Clang 22 (#3925).
- Wrapped unbraced range-for body in block before prepending loop var (#3980).
- Fixed infinite unwinding of ~list when main() lacks return 0 (#3981).
- Fixed spurious destructor warning for trivial implicit dtors (#3868).
- Fixed virtual dispatch through non-first base in multiple inheritance (#3880).
- Added missing unique_ptr members and std::extent trait (#3901).
- Added converting move ctor/assign to unique_ptr model (#3884).
- Added regression tests for polymorphic operator== via unique_ptr (#3906).
- Added and fixed C++ operational models and suppressed system headers with -nostdinc++ (#3889).
- Migrated esbmc-cpp/inheritance tests to supported test.desc format (#3885).
- Allowed unsupported extensions as the return value in C verification (#3659).
*** Function Contracts
- Implemented Function Contract Op Frame: Assigns Compliance and Loop Frame Rule (#3702).
- Fixed find_function_symbol for C++ functions (#4037).
*** Memory Model and Dereferencing
- Fixed crash on invalid bit extraction from anonymous struct with unnamed bitfield (#3985).
- Fixed crash on empty union field access from byte array (#3975).
- Fixed crash on struct-with-array-field assignment (#3971).
- Fixed spurious failure for scalar-to-struct/union type-punning (#3920).

** Solidity Frontend
- Refactored Solidity frontend (#3987).

** Verification Features
*** Interval Range Analysis (IR-IEEE)
- Added enclosure generation and solver integration for IR-RA (#3641).
- Added theorem-driven enclosure bounds and regressions (#3858).
- Guarded theorem-driven enclosure to round-to-nearest (#3871).
- Added theorem-driven support for round-to-plus-inf, round-to-minus-inf, round-to-zero, and round-to-away (#3896, #3898, #3904, #3908).
- Added theorem-driven RNE/RNA/RUP/RDN/RTZ interval lifting for ieee_add (#3927, #3940, #4021, #4026).
- Added theorem-driven RNE/RNA/RUP/RDN/RTZ interval lifting for ieee_sub (#3950, #3999, #4004, #4017).
- Added theorem-driven RNE/RNA/RUP/RDN/RTZ interval lifting for ieee_mul (#4028, #4034, #4040, #4044, #4049).
- Added theorem-driven RNE interval lifting for ieee_div (#4056).
- Renamed --ir-ra option to --ir-ieee (#3931).
- Propagated interval metadata across assignments (#3967).
- Strengthened tracked-sub interval regression expectations (#3979).
*** Symbolic Execution
- Added interval-based guard pruning (--interval-symex-guard) and made it the default (#4005, #4009).
- Added interval-based assertion pruning (--interval-symex-assert) (#4024).
- Detected writes to read-only memory in memset via __memset_impl (#3969).
- Demoted exception throw/catch logging from error/status to debug (#3913).
- Fixed guard restore across catch frame pop (#4041).
*** SMT Backend
- Updated to Bitwuzla 0.9.0 (#3994).
- Implemented quantifier support in Bitwuzla backend (#4032).
- Fixed nested __ESBMC_forall quantifiers (#3907).
- Fixed spurious array-bounds violations in nested quantifiers (#3996).
- Fixed int-to-ptr fallback for byte-updated pointer patterns (#3924).
*** Loop Invariants and K-Induction
- Enhanced loop invariant verification via combined k-induction (#3777).
- Fixed side-effect extraction when loop invariant contains function call in the middle (#3726, #3944).
- Fixed loop invariant with function calls in && chain (#3741).
- Fixed extract_invariants_near dropping all but the first loop invariant (#3956).
- Diagnosed unresolved properties on VERIFICATION UNKNOWN (#4031).
- Fixed unrolling issues (#3895).
- Fixed spurious VERIFICATION SUCCESSFUL with --multi-property --k-induction (#3862).
- Fixed misleading "process crashed" warning in k-induction parallel mode (#3682).
*** GOTO
- Extracted atomicity-check into post-conversion pass (#4048).
- Modelled C11 _Atomic assignments as separate atomic ops (#3968).
- Fixed quantifier body structure lost by remove_sideeffects for ||/&& chains (#3942).
- Fixed VLA bit-width mismatch and zero-size UB detection (#3957).
- Fixed --no-standard-checks not suppressing VLA size check (#3941).
*** Witness
- Added YAML witness parser (#3488).
- Improved method for loop invariants and added more test cases (#3900).
- Supported explicit types and location invariants (#3958).
- Improved location invariant insertion (#4012).
*** Coverage
- Fixed multi-file input ignoring extra source files (#3922).
- Applied additional coverage fixes (#3946).
- Fixed meaningless descriptions in branch-function-coverage probes (#3717).
*** Miscellaneous
- Added new intrinsic to specify unwind numbers (#3879).
- Updated command line options for concurrency checks (#4043).
- Fixed static member initialization order (#3803).
- Added --show-call-sites printing option (#3893).
- Refactored color output logic, reorganized CLI options, and improved help output (#3933).
- Added test cases for multi-property issue #2630 (#3988).

** Build System
- Added CLAUDE.md and AGENTS.md for AI coding assistants (#4003).
- Changed build script to use DebugOpt configuration (#3932).
- Restored Codecov integration with dedicated coverage workflow (#3926).
- Added GNU Info pages build script and workflow (#3722).
- Enforced per-test timeouts in regression runners and improved timeout diagnostics (#3797, #3793).
- Fixed CTest test case generation for C and C++ (#3737, #3877).
- Changed std::format to fmt::format for compiler compatibility (#3959).
- Updated LLVM installation to version 18.
- Fixed release action and included additional release documentation (#3654).

** Documentation
- Added ESBMC-Python documentation pages (#3963).
- Replaced Hugo shortcodes with plain Markdown in Python docs (#3965).
- Fixed Python documentation (#3964).
- Fixed missing #include <limits.h> in add_one contract example (#4010).
- Fixed broken Software Security course link (#3703).
- Enhanced documentation for loop invariants in ESBMC (#3954).
- Included release workflow link in releases (#3655).


*** ESBMC v8.1 Release Notes
This release of ESBMC v8.1 continues to expand the Python frontend with new data types (enum, Decimal), extended library support (math, string, list, tuple), lambda and higher-order function improvements, and numerous bug fixes for robustness. The release also introduces C/C++ verification improvements including pointer-to-member support, volatile checks, function contract enhancements, and a new time.h operational model. Below is a summary of the new features, enhancements, and bug fixes:

* New Features
** Python Frontend
*** Enum Support
- Added enum support with struct-based modeling (#3645).
*** Decimal Type
- Added Decimal construction support (#3577).
- Implemented Decimal operators: equality, ordering, and arithmetic (#3587).
*** Dictionary Enhancements
- Added initial support for dict.items() in for-loops with type-aware lowering (#3648).
*** List Operations
- Added list.remove(), list.copy(), list.sort(), and list.reverse() methods (#3535, #3540, #3632).
- Implemented sorted() built-in function (#3468).
- Added initial support to convert list(range()) expressions (#3496).
- Optimized list comparison (#3471).
- Added list comprehension support in assert statements and function call arguments (#3463, #3618).
- Fixed negative indexing on mutated lists and out-of-bounds handling (#3612, #3614, #3615, #3616).
- Fixed crash for list indexing and slicing (#3631).
- Fixed list_remove mutating type_map across branches (#3544).
- Fixed 'not list' truthiness check via list_size() instead of pointer cast (#3545).
- Fixed negative indices and parameter type inference in list slicing (#3547).
*** String Operations
- Added str.format() and format_map() support (#3446).
- Added additional Python string method support with regression coverage (#3445).
- Supported list literals in str.join() (#3575).
- Added string slicing with step support, e.g., [::-1] (#3598, #3613).
- Fixed string repetition handling (#3548).
- Fixed len() for f-strings to avoid strlen unwinding (#3543).
- Fixed string slicing with out-of-bounds indices and pointer parameters (#3582).
- Fixed string-annotation regression by supporting PEP 604 in string annotations (#3550).
- Fixed join() failing when argument comes from split() call (#3584).
- Fixed split on BinOp expressions (#3561).
- Raised IndexError on out-of-bounds string indexing (#3576).
*** Tuple Enhancements
- Added tuple membership operator support (#3457).
- Added min/max support with tuples (#3456).
- Inferred tuple return type for unannotated functions (#3470).
- Fixed tuple negative index support (#3451).
*** Set Operations
- Added set(iterable) support with bounded strnlen (#3519).
*** Math Module
- Added support for imported math functions: sin, cos, sqrt, exp, log (#3498, #3500).
- Added type checking for math.comb() (#3502).
- Expanded math library coverage with additional functions and regression tests (#3534, #3537, #3538, #3542).
- Fixed math.sqrt() domain check causing segfault (#3503).
- Fixed math constants precision (#3583).
*** Lambda and Higher-Order Functions
- Extracted lambda operations to dedicated python_lambda class (#3460).
- Added initial support for Callable function pointer variables (#3477).
- Fixed nested lambda closure variable access (#3464).
- Fixed lambda type inference and ternary expression handling (#3467).
*** Type Inference
- Extended type inference for partial generic container annotations (#3473).
- Inferred type of unannotated assignments from all RHS expressions (#3481).
- Supported constructor parameter inference for calls in compound expressions (#3505).
- Supported type inference for nondet_* and Call nodes in list elements (#3564).
- Allowed untyped parameters in nested functions (#3494).
- Added proper support for type objects, identity comparisons, and isinstance semantics (#3528).
- Improved undefined variable error messages (#3472).
*** Exception Handling
- Extracted exception handling into dedicated python_exception_handler class (#3573).
- Improved exception hierarchy to match Python standard library (#3516).
- Added support for raising arbitrary values in raise statements (#3483).
- Handled try/except ImportError for missing modules (#3572).
- Fixed crash when raising exceptions without arguments (#3514).
*** Class and Object Support
- Supported class method calls without instance (#3482).
- Fixed Optional type wrapping for functions with mixed value+None returns (#3585, #3590).
*** Built-in Functions
- Implemented optimized min() and max() built-ins with type-aware dispatch (#3443).
- Supported range() objects by converting to lists and using proper len() (#3511).
- Fixed enumerate transformation and scope/type inference (#3495).
*** Non-deterministic Values
- Added support for nondet_list and nondet_dict in pytest case generation (#3458).
- Fixed nondet_dict (#3478).
*** General Bug Fixes
- Fixed internal failure when assigning different types to the same variable (#3586).
- Fixed starred unpacking (#3611).
- Prevented crash on incompatible type reassignment (#3555).
- Various Python frontend bug fixes (#3558, #3565, #3600, #3601, #3602, #3605, #3606).
*** Regression and Testing
- Added HumanEval test cases 10-20 and documented current limitations (#3476).
- Added ai-generated-code regression suite.
- Added benchmarks from MOPSA suite.

** C/C++ Verification
*** Language Support
- Added support for pointer-to-member and pointer to member function (#3425, #3546).
- Added support for volatile checks (#3604).
- Performed linking and extern cleanup (#3484).
- Updated C++ signature for tuples and arrays (#3491).
- Fixed BuiltinTemplate triggering errors (#3489).
- Fixed default alignment crash (#3532, #3569).
*** Function Contracts
- Implemented Function Contract Replace Call Mode - Phase 2 (#3429).
*** Operational Models
- Added time.h operational model (#3452).

** Verification Features
*** Loop Handling
- Added verbose output for pragma unroll (#3490).
- Re-inserted side effects before each ASSERT/ASSUME in loop invariants (#3643).
- Fixed crash on LoopHintAttr with unsafe value pointer (#3644).
*** Verification Process
- Ask solver for LHS values when ESBMC fails to generate a constant (#2679).
- Fixed missing checks when using call.ret (#3571).
- Added --incremental-bmc when test.desc line 3 is empty (#3515).
*** Simplifier Enhancements
- Fixed member access simplification through bitcast expressions (#3493).
*** SMT Backend
- Handled address_of on constant_struct in SMT encoding (#3591).

** Build System
- Updated CI to Ubuntu 24.04 (#3506).
- Refactored build.sh and migrated ARM CI to GitHub's ARM runner (#3574).
- Disabled backtrace functionality on non-GLIBC platforms (#3531).
- Fixed x86/x86_64 detection in breakpoint.h instead of excluding ARM (#3530).
- Prioritized build-dir includes over source-dir for generated headers (#3603).
- Cleaned up temp dirs on signal-based termination (#3455).
- Implemented safer config file loading (#3492).
- Avoided compiler limit: blocks nested too deeply (#3474).
- Fixed order of operations when assigning result of builtin functions (#3568).

** Documentation
- Updated function contracts documentation for annotation feature (#3518).
- Added results and awards for Test-Comp 2025.
- Documented Python program verification with ESBMC.


*** ESBMC v8.0 Release Notes
This major release of ESBMC v8.0 delivers Python frontend enhancements with comprehensive type system improvements, advanced string handling, and dictionary support. The release includes improvements in verification capabilities, simplifier optimizations, support for witness validation, and enhanced C/C++ verification. Below is a summary of the new features, enhancements, and bug fixes:

* New Features
** Python Frontend
*** Type System Enhancements
- Added comprehensive support for Union type annotations and PEP 604 union syntax (#2914, #2917, #2938).
- Implemented TypedDict support in conversion phase (#3441).
- Added support for typing.Literal with comprehensive regression tests (#3009, #3017).
- Improved type inference for generator expressions, list comprehensions, and nested functions (#3325, #3128, #3220, #3227).
- Enhanced parameter type inference from function calls, binary operations, and list literals (#3292, #3383, #3391).
- Added subscript type inference for dictionaries and improved type propagation (#3280, #3374, #3378).
- Fixed Optional type handling across multiple contexts, including primitives and union types (#2873, #2874, #2882, #2905, #2942, #3080, #3171, #3308).
- Improved type resolution for imported classes and module-qualified annotations (#2968, #3117, #3167, #3340).
- Added strict type checking flag for primitive type validation (#3025).
- Extracted Python type definitions to a shared header for better maintainability (#3421).
- Treated typing module types as transparent to prevent processing errors (#3442, #2930).
*** Dictionary Support
- Implemented comprehensive dictionary support using parallel list representation (#3175).
- Added dictionary literal and subscript support (#3172).
- Implemented dict.get(), dict.keys(), and dict.values() methods (#3364, #3372, #3373).
- Added support for nested dictionaries via pointer storage (#3281).
- Fixed dictionary iteration in for loops with proper type inference (#3333, #3378).
- Implemented len(dict) support (#3203).
- Added del statement support for dictionary keys (#3173, #3184).
- Fixed dictionary comparison to use order-independent semantic equality (#3370).
- Improved dictionary type resolution across all annotation contexts (#3200, #3319).
- Added type-based API for nondet_dict with comprehensive test suite (#3311).
- Fixed crash when processing dictionary len() operations and using dictionaries in boolean contexts (#3371).
- Resolved dict value types from function return annotations (#3336).
- Fixed dictionary subscript value extraction in arithmetic expressions (#3246).
*** String Operations
- Created dedicated string operational model and handler classes (#2927, #2923, #3318).
- Added support for str.split() with comprehensive regression tests (#3356, #3365, #3397, #3419).
- Implemented str.join() method with string concatenation (#3016).
- Added support for str.replace() with regression tests (#3357).
- Implemented string methods: upper(), lower(), strip(), lstrip(), rstrip(), index(), rfind() (#3283, #3384, #3389, #3393, #3394, #2920, #2996).
- Added string query methods: isalpha(), isdigit(), isspace(), islower() (#2887, #2884, #2919, #2995, #2990).
- Fixed string slicing with missing bounds and parameter slicing (#3208, #3109, #2982).
- Improved string membership checks using strchr and strstr (#2946, #3143).
- Enhanced string concatenation with compound assignment and symbolic values (#3105, #3187).
- Fixed single-character string handling across multiple contexts (#3092, #3346, #3149, #3142).
- Added string module constants model (#3315).
- Fixed string comparison and type handling (#3300, #3303, #3293, #3097, #3066, #3107).
- Implemented symbolic string variable support (#3409).
*** List and Collection Operations
- Added list comprehension support with nested lists and function calls (#3128, #3415, #3416, #3417).
- Implemented list.extend(), list.clear(), and list.pop() methods (#2924, #3037, #3215, #3402, #3404).
- Added support for list concatenation (l1 + l2) (#2890).
- Fixed list repetition with symbolic size and function parameters (#3361, #3327, #3400).
- Improved list membership checks for various types (#2878, #2902, #3007).
- Enhanced list handling for pointer types and storage (#3138).
- Fixed list comparison when function calls return lists (#3210).
- Started moving Python lists into Symex for better verification (#3096).
- Optimized list operations by reducing redundancy (#3241).
- Added support for heterogeneous list comparison (#3381).
- Fixed len(list) resolution for untyped variables (#3437).
- Extended list comprehensions to handle empty lists (#3426).
*** Set Operations
- Added minimal set support with creation and operations (#2985, #3061).
- Implemented set operations (-, &, |) in dedicated python_set class (#3216, #3219).
- Added type inference for set literals (#3062).
- Fixed len() calls on set types (#2991).
*** Tuple Support
- Added initial tuple type support (#2959).
- Implemented tuple unpacking (#3101).
- Extracted tuple operations to dedicated tuple_handler (#3102).
- Aliased Tuple to tuple for compatibility (#3221).
- Fixed type inference for tuple unpacking from function calls (#3065).
*** Built-in Functions
- Implemented all() and any() built-in functions (#3260).
- Added divmod() built-in function support (#3059).
- Extended chr() builtin for variable arguments (#3103, #3133).
- Added int() builtin support to string model (#3094).
- Improved hasattr() handling and refactored into symex (#3289).
*** Class and Object Support
- Added init to class construction with proper handling (#3049, #3075).
- Implemented support for class forward references and imports (#3340, #3070).
- Fixed nested attribute chain method calls (#2977).
- Improved constructor handling with temporary variable as self (#3382).
- Fixed method parameter resolution for classes with the same method names (#3084).
- Added type annotations to instance attributes for class-typed parameters (#3002).
- Handled nested constructor calls as function arguments (#2998).
- Fixed crash when init calls methods defined later (#2972).
- Improved AttributeError reporting for missing methods (#3005).
*** Function and Control Flow
- Added nested function support with closure semantics (#3247).
- Improved type inference for nested functions and return statements (#3220, #3227, #3270, #3204).
- Fixed forward reference handling for methods in the same class (#3024).
- Added support for @overload functions with Literal arguments (#3100).
- Extended support for lambda expressions and generator expressions (#3325, #3426).
- Fixed crash when function call used as if-statement condition (#3131).
- Improved handling of keyword arguments and function calls (#3104, #3115, #3018).
- Added required argument validation for function calls (#3022, #3060).
- Fixed user-defined functions being converted to builtins (#3230).
*** Import System
- Fixed relative imports and module resolution (#2918, #2904).
- Improved import handling for local modules over system modules (#3124).
- Fixed recursive module import handling (#2907).
- Recursively processed transitive imports in astgen (#3166).
- Added support for default function arguments in cross-module calls (#3163).
*** Math Module
- Added math.sqrt() support (#3058).
- Moved math operations to python_math class (#3055).
- Extended Taylor series from 6 to 8 terms in exp/log functions (#2864).
*** Exception Handling
- Fixed exception catch for macOS different behavior (#2969, #2945).
- Fixed crash with custom exceptions (#3190).
- Properly handled KeyError exceptions for dict operations (#3184).
*** Non-deterministic Values
- Added nondet_str() for non-deterministic strings (#3185).
- Implemented nondet_list() operational model (#3186, #3188, #3189).
- Added type-parameterized nondet_list support (#3189).
- Added nondet_dict with type-based API (#3311).
- Added support for nondet_str in pytest generation (#3408).
- Fixed nondet_str materialization before address-of (#3350).
*** Code Quality and Compatibility
- Fixed Python 3.14 compatibility (#3413).
- Replaced deprecated ast.Str/ast.Num with ast.Constant for Python 3.8+ (#3422).
- Added Python code style enforcement with Yapf in CI (#2716).
- Fixed symbol dependencies system (#2782).
*** Operational Models
- Added implementation for __VERIFIER_nondet_memory (#3438).
- Added datetime module operational model (#2951).
- Added deterministic handlers for common regex patterns (#3023).
*** Type Inference Improvements
- Fixed type inference for boolean operations (and/or) in unannotated functions (#3360).
- Improved type inference for loop variables in preprocessor-transformed for loops (#3377).
- Added support for isinstance(x, type(None)) (#3376).
- Handled isinstance with tuples (#2940).
- Fixed isinstance() for string/array types (#3399).
- Implemented runtime type checking via isinstance injection (#3202).
- Fixed handling for --is-instance-check flag (#3329).
*** Function Calls and Parameters
- Inferred parameter types for stub functions without bodies (#3406).
- Detected conflicts between positional and keyword arguments (#3018).
- Extended support for keyword-only arguments (#3083, #2917).
- Fixed keyword-only parameter resolution in list iteration (#3264).
- Improved handling of * in parameters (#2917).
*** Regression and Testing
- Added Quixbugs benchmark for Python verification (#3152).
- Integrated HumanEval test cases for ESBMC Python verification (#3030).
- Added cover properties for reachability analysis (#3148).

** C/C++ Verification
*** Function Contracts
- Added Function Contract Support with comprehensive implementation (#3266).
*** Operational Models
- Fixed exit() to comply with C standard memory reclamation (#3430).
- Implemented operational models for setlocale, bindtextdomain, and textdomain (#3435).
- Added implementation for __VERIFIER_nondet_memory (#3438).
- Added ffs operational model (#2939).
- Implemented operational models for setlocale, bindtextdomain, and textdomain (#3435).
- Fixed exit() to comply with C standard memory reclamation (#3430).
*** Language Support
- Updated C++23 Support (#3050).
- Removed old frontend from the project (#2866).
*** Pointer Analysis
- Fixed false positive for dynamic offset dereference with mixed-size struct fields (#3428).
- Handled constant arrays being indexed (#3398).
*** Optimizations
- Optimized memcpy implementation (#2894).
- String container now relies on deque and string_view (#3048).
- Used __ESBMC_alloca instead of malloc in list.c (#2949).
** Build System
- Fixed Boost 1.90 compatibility by replacing boost::is_const with std::is_const (#3332).
- Changed fmt usage to explicitly format (#3254).
- Boost MPL migrated to Boost MP11 (#2954).
- Simplified CHERI build process (#3323).
- Fixed irep2 template for macOS building (#3392).
- Fixed MathSAT download links in BUILDING.md (#2925).
** Verification Features
*** Witness Support
- Implemented correctness witness validation (#3366).
- Switched back to graphml for violation witness (#3226).
- Improved witness options with new waypoint for yml format (#3108).
*** Loop Handling
- Implemented pragma unroll for loops with nested tests (#3412, #3436).
- Implemented --unwindsetname for function-relative loop bounds (#3195).
*** Verification Process
- Disabled --termination when --k-induction is specified (#3427).
- Included assertion expression in verification messages (#3348).
- Tracked and reported trivially verified assertions (#3347).
- Fixed printf format specifier type validation (#3222).
- Added --printf-check option for pointer argument validation (#3144).
*** Coverage and Testing
- Added CTest test-case generation for C coverage (#3363).
- Added support for generating pytest test files (#3257).
- Added regression tests for ctest and pytest cases generation (#3368).
- Fixed Python coverage support (#3199).
- Added documentation for HTML reports generation (#3174).
- Fixed HTML report crash (--generate-html-report) (#3165).
*** Simplifier Enhancements
- Added equality-cancellation simplifications with overflow semantics (#3317).
- Added boolean and arithmetic simplifier rewrites (#3314, #3285).
- Improved bitor2t simplifier with additional logical identities (#3306).
- Added algebraic simplifications and union WITH chain support (#3228).
- Improved arithmetic simplifier (#3268).
- Added nested conditional optimizations and condition-equivalence handling (#3276).
- Added unit tests for the simplifier (#3309).
- Fixed typo: simplied -> simplified (#3353).
- Built-in object size no longer relies on simplifier (#3330).
** SMT Backend
- Added simplifications for pointer_offset (#3229).
** Concurrency and SV-COMP
*** SV-COMP Enhancements
- Introduced new SSA branching (#3157).
- Avoided force switch (#3156).
- Supported thread local for data races check (#2984).
- Optimized race checks for function call (#2957).
- Refactored data race check (#2926).
- Added new option to simplify verification for data races check (#2889).
- Fixed zero initialization for infinite array (#2921).
- Ignored unsupported witness assumptions (#3134).
- Updated ESBMC wrapper and scripts for SVCOMP26 (#3206, #2861, #3051).
- Added new tasks for SV-COMP (#3095).
- Disabled goto-contractor and updated witness config (#3072).
** Infrastructure and CI
*** Continuous Integration
- Cleaned workflows (#3405).
- Used cache to accelerate build process (#3324, #3328).
- Optimized cache hits and switched to the appropriate runner (#3328).
- Fixed cache restore key and regularly cleaned cache (#3335).
** Documentation
- Consolidated everything into the docs (#3420, #3424).
- Added new website article (#3275).
- Implemented ESBMC website (#3269).
- Fixed pages workflow (#3271).
- Added PPA Maintenance Documentation (#3249).
- Updated date for PPA readme (#3253).
- Added coverage documentation and updated main README (#3211).
** Build Configuration
- Made 32-bit bundling optional (#3279).
- Added lib path for conda and pyenv (#3277, #3263).
- Fixed Python pytest import issues (#3261).
- Fixed Python frontend build and testing on macOS CI (#3183).
- Always used C parser to process bundled C libraries (#3169).
- Added --dont-care-about-missing-extensions flag (#2983).
** Testing Infrastructure
- Disabled test breaking Windows builds (#3180).
- Reflowed regression suite (#2863).
- Cleaned up test cases and regression tests (#2838).
- Added type assertion in constant_array2t constructor (#2952).
** Bug Fixes
*** Python Frontend Fixes
- Fixed crash when subscripting dictionary literals (#3440).
- Fixed crash when parsing list elements without a value key (#3380).
- Fixed crash with omitted optional parameters (#2874).
- Fixed crash when using isinstance in an expression (#3344).
- Fixed crash on open-ended string slice with pointer parameters (#3299).
- Fixed crash when undefined methods are used in assignments (#3064).
- Fixed crash when iterating over union types (#3029).
- Fixed crash when handling list assignments without full type annotations (#2922).
- Fixed segfault when calling len() on an optional string with a None default (#3071, #3079).
- Fixed segfault when asserting on None-returning functions (#3212).
- Fixed None comparison in lists and type-mismatched comparisons (#3369).
- Improved None and Optional handling across frontend (#2882).
- Fixed string truncation and type mismatches in ternary expressions (#3343).
- Fixed ternary expression array-to-pointer conversion (#3039).
- Fixed handling of empty width string in get_type_width on macOS (#2941).
- Fixed exception with formatted string literal (#2913).
- Fixed character comparison in functions with str parameters (#3293).
- Fixed nested dereference and type inference for string module (#3401).
- Fixed nested loop variable collision in preprocessor (#2896).
- Fixed union type handling in pointer dereference and symbolic assignment (#3403).
- Fixed overload with different fields (#3334).
- Fixed union type variable declarations with deferred assignment (#3321).
- Fixed attribute access on union type parameters (#3310).
- Fixed initialization of loop index in list comprehensions (#3417).
- Fixed handling for augmented assignments (#3342).
- Fixed boost::process compilation on macOS (#2868).
** IR and Counterexamples
- Fixed IR counterexample print (#3112).
- Included line numbers in Python stacktrace (#3291).
** General Fixes
- Fixed __ESBMC_init_object exception handling type (#2877).
- Fixed testcomp esbmc-wrapper (#3231).
* Acknowledgments
We want to thank the following contributors for this release: @lucasccordeiro, @brcfarias, @XLiZHI, @LukeW1999, @rafaelsamenezes, @prototypeC14, @sergillam, @Yiannis128, @dan-eicher, @sgpthomas, and the entire ESBMC community.

*** Release Notes for ESBMC v7.11
This release of ESBMC v7.11 delivers substantial improvements to the Python frontend with comprehensive type system enhancements, major advances in C/C++ verification and STL support, extensive simplifier optimizations, and concurrency bug fixes. The release also includes Solidity frontend improvements, SMT backend updates, and enhanced verification capabilities. Below is a summary of the new features, enhancements, and bug fixes:

* New Features
** Python Frontend
*** Type System Enhancements
- Added support for Union type annotations and PEP 604 union syntax (int | bool) (#2849, #2853).
- Improved type inference for typing.Any, class methods, and comparison operations (#2847, #2829).
- Enhanced parameter type inference from function calls for unannotated parameters (#2741).
- Added subscript type inference with comprehensive regression tests (#2705).
- Enabled strict type checking with mypy for improved code quality (#2754, #2750).
*** Exception Handling
- Comprehensive exception handling support, including proper exception object merging (#2719, #2832).
- Added support for Python's generic Exception type and AssertionError (#2753, #2749).
- Improved raise expression handling and exception semantics (#2766, #2751).
- Fixed exception handling with empty variable binding (#2734).
*** String Operations
- Added support for string operations, including 'in' operator, startswith(), and endswith() methods (#2827).
- Fixed string slicing semantics with extended regression coverage (#2837).
- Improved string comparison between pointer and array types (#2841).
- Fixed string concatenation for various char and string combinations (#2768, #2758).
- Added initial support for f-strings (JoinedStr) (#2736).
- Added initial regular expression operational model (#2836).
*** Built-in Functions and Operators
- Added support for print() function, input() function, and name built-in variable (#2830, #2696, #2727).
- Extended support for min(), max(), enumerate(), hasattr(), and chr() for multibyte characters (#2697, #2718, #2674, #2644).
- Added models for random functions (uniform, getrandbits, randrange) (#2822).
- Added math module support including floor(), ceil(), comb(), and improved math operations (#2704, #2701).
- Added os module support for mkdir() and rmdir() with OSError hierarchy (#2824).
*** Control Flow and Language Features
- Added initial support for lambda expressions (#2730).
- Implemented ternary operator support (#2721).
- Improved handling of keyword arguments and function calls in return statements (#2828, #2717).
*** List and Collection Operations
- Added support for heterogeneous lists and append operations (#2767).
- Implemented list.insert() method and list repetition with variables (#2817, #2711, #2715, #2724).
- Enhanced list handling for variable-length strings (#2714, #2706).
- Improved validation of range() in for-loops (#2708).
*** Import System
- Fixed import handling for referenced classes and mixed import styles (#2857).
- Fixed imports for fully qualified names and forward reference handling (#2815, #2738).
- Added fallback to global scope for unresolved function calls (#2709).
*** Type Correctness and Internal Improvements
- Fixed NoneType encoding and added NoneType as a type in get_type_from_constant (#2787, #2650).
- Fixed array-to-pointer decay for keyword arguments (#2844).
- Improved constructor handling with temporary variable as self (#2816).
- Fixed symbol table type updates and multiple assignment handling (#2712, #2710).
- Added __ESBMC_HIDE to models and __ESBMC_rounding_mode initialization (#2788, #2762).
- Fixed IEEE floating-point crashes and Python power operation precision (#2748).
** Solidity Verification
- Added support for UncheckedBlock keyword (#2819).
- Added Solidity Frontend README.md documentation (#2818).
- Fixed pow operation, inheritance handling, and dynamic array & contract typecast (#2802, #2745, #2733).
- Various bug fixes and regression improvements (#2799, #2731, #2726).
** C/C++ Verification
*** Built-in Functions
- Implemented __atomic_exchange_n builtin for atomic operations (#2809).
- Added support for __builtin_object_size intrinsic with full regression suite (#2774).
- Added __builtin_offsetof to clang C language frontend (#2772).
*** STL and Standard Library Improvements
- Fixed valarray implementation with symbolic and concrete verification tests (#2778).
- Optimized map::find() and operators for map and string for faster verification (#2692, #2690).
- Fixed iterator invalidation in set range erase (#2649).
- Corrected multiset to allow duplicates and fixed equal_range() (#2646).
- Fixed iterator memory safety issues in string model (#2645).
- Fixed deque reverse iterator bugs (#2643).
- Fixed stack constructor to properly initialize from container (#2648).
*** C++ Frontend Enhancements
- Improved sstream operational model and fixed stringstream compilation errors (#2683, #2681).
- Fixed wallop_type infinite recursion with cycle detection (#2671).
- Removed unnecessary T() calls for non-default-constructible types (#2668).
- Added reference adjustments to pre/post-increment/decrement operations (#2729).
** C Verification
- Added operational model for nan function (#2667).
- Improved relation simplification (#2777).
- Added rename for re-alloc size (#2806).
- Added check for empty function body (#2658).
- Improved getenv() operational model (#2653).
* Simplifier Enhancements
** Extensive simplification improvements across multiple expression types:
- Added constant propagation support for struct field updates (#2823).
- Improved concat2t::do_simplify() to detect byte_extract reconstruction patterns (#2820).
- Implemented pointer_object2t::do_simplify() and improved same_object2t::do_simplify() (#2795, #2796).
- Enhanced pointer offset simplification in VCC generation (#2803, #2793).
- Fixed same_object simplification for typecast expressions (#2791).
- Added boolean, bitwise, and relational simplification rules (#2790).
- Added associative simplification for logical AND/OR expressions (#2786).
- Added arithmetic and bitwise expression simplifications (#2785).
- Added simplification rules for self-comparisons and idempotent expressions (#2784).
- General simplifier cleanup (#2794).
* SMT Backend Enhancements
- Added CVC5 quantifier support (#2707).
- Updated to Bitwuzla 0.8.2 solver backend (#2677).
- Added initial support for byte update operations in integer arithmetic mode (#2804).
- Standardized dump_smt() interface across solver backends (#2743).
* Symbolic Execution Enhancements
- Added comprehensive realloc regression tests and fixed realloc symbolic model (#2781).
- Fixed symex_input to only process arguments matching format specifiers (#2800).
- Fixed static output_count scoping in symex_target_equationt (#2676).
* Concurrency and Multithreading Enhancements
- Fixed data races in irep, irep2, and goto trace for parallel solving (#2670, #2680, #2685, #2678).
- Fixed string container issues for parallel solving (#2647).
- Don't terminate thread in pthread_exit to match POSIX behavior (#2744).
- Fixed incremental-smt in multi-property concurrency scenarios (#2665).
- Fixed parallel solving output issues (#2652).
* Verification Process
- Loop Invariants: Added interactive loop invariant support (experimental) and fixed loop invariant scope for nested loops (#2651, #2713).
- Multi-property Verification: Enhanced verification to process properties individually using claim.cstr (#2655).
- Witness Support: Added yaml-based violation witness support (#2688).
* Fixes and Improvements
** Verification Process
- Fixed incorrect remaining VCC count after caching (#2814).
- Fixed assume constant propagation (#2759).
- Added alignment checks for direct pointer dereferences (#2684).
- Improved slice unused array updates optimization (#2722).
- Skip loops transform with pointer only when VSA is enabled (#2833).
- Fixed handling of missing interval data in goto_contractor (#2663).
- Fixed assignment and trace optimization issues (#2660, #2669).
** Operational Models
- Improved libc models for I/O and error handling (#2798).
- Optimized strncpy for BMC performance (#2682).
** Build System and CI
- Integrated LLVM 21 support (#2821).
- Corrected build instructions (#2854).
- Added fallback mirrors for GMP download in CI (#2770).
- Fixed YAPF checkout for PR from fork repositories (#2760).
- Fixed macOS build issues (#2739).
** Testing and Infrastructure
- Cleaned up test cases and regression tests (#2838).
- Updated big-int fuzzing test (#2659).
- Fixed symbol dependencies system for Python frontend (#2782).
- Added Python code style enforcement with Yapf in CI (#2716).
- Ensured overflow checks work with incremental mode (#2776).
- Reverted problematic changes to maintain stability (#2691, #2687).
* Acknowledgments
We want to thank the following contributors for this release: @lucasccordeiro, @brcfarias, @XLiZHI, @ChenfengWei0, @Luke-Sanderson, @LukeW1999, @Ben-Eichhoefer, @Anthonysdu, @rafaelsamenezes, @sulaychaudhry, @prototypeC14, @intrigus-lgtm, @DevM-uk, @adilanwar2399, and the entire ESBMC community.

*** Version 7.10

This release of ESBMC v7.10 introduces significant improvements in Python and Solidity frontends, concurrency and SMT modeling, termination analysis, and C/C++ verification. It also includes numerous bug fixes and enhancements to the test infrastructure. Below is a comprehensive summary of the new features, enhancements, and bug fixes:

* New Features
** Termination Checking
- Introduced support for termination analysis via forward condition checks to detect non-terminating loops in C programs (#2628).
** Python Frontend
- Added support for isinstance() checks to improve compatibility with Python type introspection (#2627).
- Enabled symbolic support for built-in functions like ord() and super() (#2625, #2624).
- Enhanced handling of abs(), float(str), int(str), and conditional expressions (#2441, #2427, #2429, #2453).
- Extended support for numpy.matmul, numpy.dot, and symbolic math functions such as pow() and fabs() (#2487, #2460, #2506, #2435).
- Improved modeling of compound assignments, attribute access, and iterable for loops (#2509, #2508, #2458).
- Added support for bytes literals, is/is not, and function argument inference (#2484, #2480, #2494).
** Solidity Verification
- Added support for direct function calls without requiring contract instances (#2613).
- Changed the default Solidity verification mode to unbounded to allow deeper analysis (#2593).
- Improved array member call support, version handling, and modeling of selfdestruct and modifiers (#2588, #2567, #2568, #2537).
- Major cleanup of dynamic arrays and bytes implementation for better correctness and performance (#2605).
- Fixed bugs in new expressions and object invalidation during symbolic execution (#2623, #2571).
** C/C++ Verification
- Added operational models for C++ random() and improved STL support for unordered_map, bitset, char_traits, and string (#2603, #2530, #2543, #2584, #2592).
- Fixed do-while with empty body, external variable initialization, and typeid modeling (#2604, #2575, #2534).
- Improved support for exception rethrows, memory allocation traits, and iterator logic in the C++ frontend (#2550, #2536, #2526).
** SMT Backend Enhancements
- Partial support for IEEE 754-compliant real encoding for floating-point operations (#2596).
- Integrated Bitwuzla v0.8.1 solver backend and added rational value extraction in int_encoding mode (#2594, #2582).
- Fixed float-to-bv and float-to-int casting bugs in both real and integer encodings (#2576, #2577, #2581).
- Improved handling of signbit, exception diagnostics, and default solver selection with --ir option (#2595, #2585).
** Concurrency and Multithreading
- Fixed pthread_rwlock modeling and added support for pthread_cleanup_push/pop handlers (#2609, #2450).
- Improved symbolic modeling of thread-local globals and data race detection in incremental SMT mode (#2583, #2556).
* Fixes and Improvements
** Verification Process
- Improved modeling for symbolic access, memory checks, and __ESBMC_r_ok() intrinsic (#2431).
- Fixed symbolic counterexample generation and error trace crashes in SMT translation (#2570).
- Resolved typecast issues and warnings in BigInt-to-double conversions for small rationals (#2600).
** Build System
- Updated fuzzing configuration and Windows/CHERI build integration (#2606, #2447).
- Enabled precompiled headers for GCC and fixed GMP linking for solver builds (#2428, #2483).
- Addressed inconsistencies in dump_smt() across solvers and added CI support for LLVM 16 and 17 (#2524, #2436, #2432).
** Coverage and Test Infrastructure
- Added new regression tests for Python, SMT, and parallel solving scenarios (#2547, #2608).
- Added warning mechanism when previously known bugs no longer fail in test runs (#2496).
- Improved color-coded output and summaries for multi-property verification (#2586, #2620).
* Acknowledgments
We want to thank the following contributors for this release: @lucasccordeiro, @brcfarias, @ChenfengWei0, @XLiZHI, @Anthonysdu, @Ben-Eichhoefer, @prototypeC14, @Luke-Sanderson, @DevM-uk, @intrigus-lgtm, @mihaistate, @rafaelsamenezes, @yjtew, and the entire ESBMC community.

*** Version 7.9

This release of ESBMC v7.9 introduces enhancements in Solidity verification, Python frontend support, overflow and concurrency analysis, and overall system robustness. Below is a comprehensive summary of the new features, enhancements, and bug fixes:

* New Features
** Solidity Verification
- Introduced a bounded cross-contract verification algorithm for more comprehensive smart contract analysis (#2327).
- Added support for function calls with options, unit keywords, and insufficient balance checks in Solidity (#2398, #2393).
- Implemented coverage support for Solidity programs, enabling fine-grained analysis (#2389).
- Introduced AST merging across multiple files and fixed function order bugs, improving multi-contract verification accuracy (#2392, #2400).
- Improved address modeling and ensured temp files are uniquely created to prevent race conditions (#2379, #2396).
** Python Frontend
- Enhanced support for NumPy math functions by reusing C libm models (#2395).
- Added models for numpy.ceil, improved broadcasting rule checking, and better support for dtype arguments (#2382, #2353, #2300).
- Implemented support for nondeterministic values, random.random(), random.randint(), and improved function call handling (#2303, #2299, #2250).
- Enabled function default parameters to be variables and improved string literal handling (#2346, #2251).
** C/C++ Verification
- Added operational models for C++ constructs like std::stoi, std::stof, and align_val_t (#2277, #2301).
- Improved realloc handling and added overflow detection for comparison operators (#2345, #2344).
- Enhanced typecast overflow detection and introduced overflow_cast in SMT backend (#2376, #2367).
** SMT Backend Enhancements
- Fixed overflow detection for signed subtraction and unsigned division/modulus (#2383).
- Enhanced overflow handling in symbolic execution (#2338, #2343).
- Supported bitwise integer arithmetic in Z3 (#2354).
- Added support for SMT quantifiers (#2261).
** Concurrency and Data-Race Detection
- Improved concurrency checks by optimizing and unifying the data race flags (#2385, #2399).
- Increased context-switch bound for SV-COMP to 3 (#2378).
* Fixes and Improvements
** Verification Process
- Fixed regression in Solidity verification (#2402).
- Improved modeling of strcpy, atexit, and infinite arrays for operational models (#2253, #2351, #2349).
- Fixed symbolic execution issues with goto-check and k-induction under certain edge cases (#2328, #2326, #2340).
* Build System
- Fixed build issues on Windows (#2403).
- Updated external dependencies and improved CMake compatibility (#2390, #2370).
- Made test cases compatible with Windows (#2361).
* Coverage and Test Infrastructure
- Fixed the internal coverage algorithm and improved Solidity coverage instrumentation (#2365, #2389).
- Added various regression and SV-COMP benchmark test cases (#2362, #2359, #2318).
* Acknowledgments
We want to thank the following contributors for this release: @XLiZHI, @ChenfengWei0, @prototypeC14, @brcfarias, @intrigus-lgtm, @Ben-Eichhoefer, @ssshivaji, and @lucasccordeiro. Your contributions to Solidity support, Python frontend, SMT enhancements, and concurrency modeling have significantly strengthened the ESBMC verification ecosystem.

*** Version 7.8.1

This is the ESBMC version used at the FSE'25 submission:

- Feature/build mac (#2219)
- GCSE now only caches overflow inner operands (#2221)
- Only replace inner expressions for overflow in GCSE (#2227)
- Handling chained comparisons in Python (#2228)
- GCSE now resets index2t (#2230)
- Force update of tags in benchexec action (#2234)
- Added new catch exception for GCSE (#2233)
- Improve the adjustment of capture variables (#2222)


*** Version 7.8

This release introduces several significant improvements, feature enhancements, bug fixes, and updates to improve the functionality and usability of ESBMC. Below is a detailed breakdown of the changes:

* New Features
** Build Support for macOS:
- Added build instructions for macOS M1 and Intel architectures (#2217, #2216, #2213).
- Updated README files to reflect new macOS build compatibility (#2213, #2089).
** SMT Solver Enhancements:
- Support for extracting arrays from tuples in SMT (#2215).
- Updated Bitwuzla SMT solver from v0.6.1 to v0.7.0 for improved performance (#2199).
- Fixed pointer typecast issues in SMT backends for byte updates (#2197).
** Concurrency Improvements:
- Adjusted concurrency flags for memory leak and overflow checks (#2206).
- Read global variables directly from function calls in concurrency checks (#2192).
- Fixed interleavings and guards for better thread scheduling (#2185).
- Introduced a new thread scheduling policy (#2178).
** C and C++ Verification Enhancements:
- Added support for clang built-in float16 types (#2214).
- Support for clang::__builtin_va_* operations in C verification (#2207).
- Fixed allocation size calculations in C++ new operations (#2187).
- Enhanced lambda captures for C++14 (#2170).
- Supported std::make_tuple, std::forward, and other C++ standard functions (#2051, #2118).
** Python Frontend Updates:
- Improved handling of module aliases during verification (#2196).
- Enhanced error messages and documentation for Python (#2107, #2086).
* Fixes and Improvements
** Verification Process:
- Improved constant propagation handling (#2128).
- Addressed robustness issues in alloca handling during symbolic execution (#2095).
- Enhanced handling of array initialization loops in C++ verification (#2101).
** Build and Compilation:
- Fixed compatibility with newer Clang versions (Clang 18 and Clang 19) (#2189, #2099).
- Updated CI to include static builds with LLVM 16 as the default (#2062).
** Coverage and Benchmarks:
- Enabled assertion coverage in function mode (#2106).
- Added benchmarks for SV-COMP 2025 (#2158).
- Improved branch coverage support (#2056).
* Miscellaneous:
- Hardened utility functions like binary2integer for reliability (#2132).
- Added JSON generation for test reports and refined HTML reports (#2127).
- Updated concurrency benchmark inclusion in BenchExec runs (#2201).
* Acknowledgments
This release would not have been possible without the contributions from the community and team members, including but not limited to @ssshivaji, @intrigus-lgtm, @XLiZHI, @ChenfengWei0, @Anthonysdu, @mikhailramalho, and @brcfarias. Thank you for your continued support and efforts to enhance ESBMC.

*** Version 7.7
* New Features and Improvements:
** Python Frontend:
- Enhanced type inference and fixed indexing issues (#2017, #2002).
- Handling single-type lists (#1957).
- Supported additional Python built-in functions like int.bit_length() and string concatenation (#1935, #1941).
- Fixed handling of Python process creation on Windows (#1950).
- Enforced Python 3 compatibility (#1983).
** Clang C++ Frontend:
- Added support for CXXStdInitializerList and list constructors in vectors (#2039).
- Introduced support for std::isnormal function (#2032).
- Updated support for isnan function and operational models (#2009, #2008).
- Resolved issues with implicit copy and move constructors in unions (#2016).
- Fixed return types for CXXMemberCalls and improved lambda function support (#2003, #1971).
- Improved support for pseudo destructors and array type initialization (#1975, #1968).
** Solidity Frontend:
- Supported Solidity import statements (#1927, #1926).
- Enhanced contract type variables and mapping data structures (#1917, #1867).
- Introduced support for Solidity event keywords (#1872).
** Concurrency:
- Avoided forced switching in the built-in library to enhance performance in multithreading scenarios (#2025).
- Improved race condition detection, including using the address for race checking and handling __VERIFIER_assert (#1995, #1953).
- Optimized pointer analysis for global reads and writes (#1958).
** Coverage Analysis
- Update Condition Coverage Calculation Strategy (#1999).
* Bug Fixes:
** Build & Compilation:
- Resolved unused variables in the build process (#2031).
- Fixed various Fedora build issues and updated build instructions (#1994).
- Fixed CHERI build errors and updated CHERI build instructions (#1984, #1974).
- Addressed Python process creation issues on Windows platforms (#1950).
** Concurrency:
- Fixed forced switching in built-in libraries for multithreading (#2025).
- Adjusted race checking for GOTO instructions and symbolic execution (#1995, #1940).
** Frontend Enhancements:
- Corrected implicit copy/move constructor bodies in the Clang C++ frontend (#2016).
- Updated operational models for mathematical functions (#2009, #2008).
** Miscellaneous Fixes:
- Fixed README documentation (#2038).
- Addressed issues with HTML reports (#2019).
- Updated and fixed CI/CD actions for release automation (#2027, #2026).
** CI/CD Improvements:
- Updated benchexec and upload artifact actions (#2026, #2023).
- Addressed release action issues for smoother deployment (#2027).
** Documentation:
- Fixed and updated BUILDING.md with instructions for Yices and CVC5 (#1855, #1852).
- Added Python frontend documentation (#1880).

*** Version 7.6.1
* Clang C/C++ Frontend
- Interpret option -Wc,OPT1,OPT2,... as passing OPT1 OPT2 ... to the clang frontend directly (#1840) 
- Fix additional C++ APIs: [sf]stream, valarray, locale  C++ OM (#1834) 
- Fix some more C++ APIs: bitset, csignal and string_view  C++ OM (#1832)
- fixed std::move functions call (#1827)
* Solidity Frontend
- Bug fixing and code refactoring (#1839)
- Support Solidity built-in variables and functions (#1828)
* General Improvements
- Added total VCCs column (#1841)
- Improved build instructions about ESBMC-CHERI (#1833)

*** Version 7.6
* Clang-C/C++ Frontend
- Support "noexcept" keyword (#1819)
- Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 (#1817)
- Support compilation against LLVM-17 and -18 (#1816)
- Support more type of exception var (#1815)
- Param name in parameter packs (#1813)
- Fix unnamed parameter (#1812)
- Support throw decl (#1806) 
- Fix member init ref (#1802) 
- Add exception id for catch (#1799)
- Add frontend support for some constructs used in the Linux kernel (#1798) 
- Support builtin template (#1789) 
- Fix recursive structs (#1781)
- Fix the order of params (#1780)
- Handle recursive conversion in base type  C++ (#1777)
- Support empty list initializer for scalars (#1775) 
- Support CXXThrowExpr node (#1768) 
- Adjust return type for ref type (#1766)
- Fixed seg fault caused by extern (#1765) 
- fixed wrong enum type (#1759) 
- Simplify if conditions (#1756)
- Add delegating constructors  help wanted (#1754)
- Add support for anon constructors in anon structs (#1753)
- Support variable template specialization (#1748)
- Add support for nullptr_t (#1745)
- Remove <type_traits> + support C++17 variable template declarations  C++ OM (#1739)
- Avoid the temporary object (#1736) 
- Support sizeof expression (#173)
- Fix base classes and tmp object (#1715)
- Add new node for CXXDefaultInitExprClass (#1705) 
- Fix compilation errors for the <numeric> lib (#1702)
- Fix compilation errors for set (#1700) 
- Fix cpp if-else typecast (#1692)
- Fix compilation errors and warning messages in the <queue>lib (#1691)
- Fix assertion failed in string OM (#1686) 
- Fix various warning/compilation errors for <iterator> and <string> libs (#1685)
- Enable test case for the Typeinfo lib (#1681)
- Standardize the cpp new/delete (#1670)
- Add memory deallocation check (#1671)
- Add <string_view> model (#1672)
* Python Frontend
- Support for class methods (#1808) 
- Convert "for v in range(start, end, step)" (#1804) 
- Add type annotation to methods (#1800)
- Handle longer arithmetic expressions (#1795)
- Variable initialization via ** operator and uint64() function #1791
- Replace abort() with warning for undefined functions (#1763)
- Add support for len() (#1757)
- Support for "break" and "continue" (#1752) 
- Add support for "bytes" type and array indexing (#1744)
- Add support for float numbers (#1734) 
- Handling imports (#1714)
* Interval Analysis
- Optimization of Interval Analysis (#1755)
- Widening fixes (#1738)
- Add message for interval analysis duration (#1790)
- Support for symbolic reconstruction of expression (#1726)
- Make interleavings unviable after the main thread has ended (#1721)
- Fixed relation >= and > for wrapped intervals (#1712)
- Fixes for interval bitwise arithmetic (#1711) 
- < and <= fixes for Wrapped Intervals (#1662) 
*Concurrency Support
- Do not record __ESBMC_pthread_thread (#1733)
- Do not record __ESBMC_rounding_mode (#1732)
* Solidity Frontend
- Bug fixed for constructor and struct (#1788) 
- Fix the missing contract name in the symbol id (#1697) 
* General Improvements
- Restore LTL code (#1586)
- Fix atomic_begin and atomic_end translation (#1821) 
- Fix macOS CI build (#1809)
- Fixes for CHERI builds  cheri (#1786)
- Add incremental smt support for CVC4 (#1773)
- Fixed seg fault in error trace (#1764) 
- Add --segfault-handler dumping a stack trace and memory map on SIGSEGV and SIGABRT (#1760)
- Convert references more consistently C++ (#1696) 
- Fix the wrong usage of equality instead of assignment smt (#1689) 
- Extend regdb.py with categorized flags and allow querying using glob patterns (#1684)
- Support detecting Clang resource dir for >= v16 (#1682)
- Add tool regdb.py for regression test management (#1680) 

*** Version 7.5
* Clang-C++ Frontend
- Improved C++ dangling pointer checking (#1648).
- Improved C++ double delete (#1648).
- Fixed the cpp new initialization (#1636).
- Fixed the copy and move constructor (#1614).
- Support rvalue references C++11 (#1595).
* Solidity Frontend
- Support Multiple Contract Verification (#1640).
- Bug fixes for Inheritance (#1624).
- Scope fix (#1606).
- Support Error Handling (#1598).
- Supported struct data structure and fixed bugs (#1563).
- Fixed nested loop and one-statement block (#1546).
- Fixed Visibility (#1545).
- Support pattern-base checking in contract mode (#1543).
- Continue and Break Keyword Supported (#1529).
* Python Frontend
- Inheritance and overriding (#1639).
- Empty class instantiation and built-in functions support (#1608).
- Support pass statement and var declarations without initialization (#1602).
- Support for Class attributes (#1587).
- Class definition and instantiation (#1552).
- Support for // operator (#1522).
- Add type inference for dynamic variables (#1515).
- Python frontend: Add support for recursion (#1481).
- Adjust types and re-enable tests (#1441).
- Add support for non-determinism (#1439).
- Optimize --function handling (#1438).
- Add support for conditional operator and function flag (#1437).
* Jimple frontend
- Jimple throws are now shown at --show-claims (#1632).
* Abstract Interpretation
- Interval analysis now inverts boolean correctly (#1625).
- VSA is now only computed with GCSE flag (#1607).
- Instrumentation for interval loop invariants (#1603).
- Wrapped intervals can now optimize expressions (#1566).
- Support for context-aware intervals (#1564).
* GOTO contractors
- Ibex fixpoint was causing crashes; fixed-point is done manually now (#1638).
- Integers (signed and unsigned) and floats are converted from one to another correctly now (#1638).
* Concurrency
- Fixed monolithic partial order-reduction (#1633)
- Optimize the efficiency of data race detection (#1544).
- Support for "printf" for data races check (#1477).
- Take cur_state->guard into account for creating a new thread (#1463).
- Fixing dereference in data-races check (#1460).
- Optimize index races check (#1456).
* Operational models
- Add libm musl float OMs used in svcomp24 (#1601).
- Fix range of rand() and random() to include upper endpoint (#1596).
- Add Operational Model for semaphore (#1536).
- Added sscanf OM (#1519).
- Add OM for pthread_rwlock_rdlock (#1516).
- Rework of the support for builtins (#1435).
* Memory model
- Pass alignment attribute constraint through to smt (#1593).
- Value-set considers alignment of references to symbols (#1629).
- SMT memspace fixes (#1538).
- Fixed crash caused by invalid id in value set (#1514).
- Distinguish between valid-memsafety and valid-memcleanup (#1482).
- Infinity array bounds are no longer checked (#1432).
* General improvements
- Added missing unwinding assertion loopid (#1635).
- Protect make_n_ary() from being called with empty list (#1627).
- Fixed overflow in ID node from witness generation (#1623).
- Fixed incorrect assertion coverage (#1619).
- SV-Comp builds includes all supported solvers (#1613).
- Remove shared_ptr from being used unnecessarily in API (#1612).
- Improved build instructions for ESBMC-CHERI (#1611).
- Performance improvement for multi-property verification (#1605).
- Update Bitwuzla to v0.3.1 (#1604).
- Show decision runtime for each claim (#1578).
- Added ARM64 build into CI (#1575).
- Fixed overflow- encoding (#1560).
- Fix the general case for string-literal to array conversion (#1549).
- Update Boolector to v3.2.3 (#1542).
- Simplify BigInt power2 API (#1532).
- Do not overwrite location of first instruction during goto-conversion (#1530).
- Optimize floats memset for zero initialization (#1509).
- Intrinsic memset claim fix (#1506).
- Interpret non-adorned fptrs in function argument list (#1503).
- Add __ESBMC_unreachable() and --enable-unreachability-intrinsic (#1502).
- Interpret __builtin_unreachable() as no-op for sv-comp (#1500).
- Fixed wrong line number in if-then-else (#1491).
- Put some effort into representing array_of terms to the user (#1488).
- symex_input: use source location of intrinsic for assignments (#1472).
- Added short circuit for one byte types in optimized memset (#1467).
- strerror: fix integer overflow (#1457).

*** Version 7.4
* Python Frontend
- Support for logical and/or (#1423)
- Handling asserts (#1420)
- Function definitions/calls (#1419)
- Add support for GtE, LtE, and mod operators (#1414)
- While statements (#1406)
- If/else support (#1396)
- Initial implementation of Python frontend (#1390)
* Operational Models
- RFC: Low-precision models for log() family, exp() and pow() (#1421)
- <fenv.h> only use own definitions on FreeBSD (#1417)
- Add models for frexp() and ldexp() (#1413)
- Replaced malloc with __ESBMC_alloca in getenv (#1250)
* Abstract Interpretation
- Interval Analysis unit tests now deletes migration reference (#1409)
- Interval now uses std::optional to keep the bounds (#1407)
- CNF generation no longer removes typecast (#1393)
- Support for symbol expressions during interval analysis (#1330)
- Support for symbol expressions during interval analysis (#1330)
- Interval expression generation for floats (#1327)
- Interval Analysis assumptions now only uses local symbols (#1319)
- Propagation of Boolean Intervals (#1313)
- Interval singleton propagation (#1305)
- Make Interval Analysis reset state after pointer operation (#1234)
* Solidity frontend
- Support "require" keywords (#1321)
- Verify the contract as a whole (#1309)
- Set the class/contract name for function verification (#1304)
- Solidity frontend update (#1298)
* SMT backend
- Added Bitwutzla 0.2.0 to ESBMC (#1318)
- Bring smtlib backend on par with other backends (#1237)
- Fix emitting bvsgt (#1235)
- fp_conv: fix gte: not(less) is not equiv to get (#1227)
- Changed smtlib linker flags (#1216)
* Concurrency
- CUDA verification: Support for more TCS (#1314)
- Analyze global variables for goto instructions during symex (#1276)
- CUDA OM: replaced __ESBMC_alloca with infinite array size (#1275)
- Remove unviable interleaving (#1269)
- Kernel concurrency model - SPIN LOCK (#1268)
- Do not produce interleavings after __ESBMC_main ends (#1265)
- CUDA: Add CuDNN OM (#1260)
- CUDA OM: Clean up and optimize the CUDA operational models #1258
- Guard fix (#1242)
- Add benchmarks for CUDA (#1228)
* Memory Safety
- Enhance the memsafety analysis (#1295)
- Add memory cleanup check (#1273)
- Add option to avoid checking memory-leaks on abort() (#1270)
* General Improvements:
- Unions are not required to have an init member anymore (#1427)
- Empty loops are now converted to assume 0 (#1412)
- Counter-example: only recurse if generating a sub-expr has been possible (#1410)
- Adhere to C semantics for pointer-arithmetic (#1402)
- FreeBSD/CheriBSD compatibility (#1397)
- Simplify irep1: do not resolve index on constants under addr-of #1376
- Unify simplification of modulus2t with div2t (#1360)
- Support bit-casting to multi-dimensional arrays (#1358)
- --unwindset refine (#1306)
- Allow more fine-grained control over debug log messages (#1281)
- Add memory consumption metrics (#1272)
- Make irep2 construction a bit more C++ (#1264)
- K-induction fix (#1218)
- Show the exact location of function call (#1217)

*** Version 7.3
* Clang CHERI-C frontend
- Prepare CHERI-C support (#905).
* Abstract Interpretation Framework:
- Revamp on interval analysis options (#1153).
- Replaced cmath with its cpp counterpart (#1073).
- Interval Analysis: the get_interval function is more generic (#1065).
- Fixed wrong computation for type bounds (#1052).
- Abstract interpretation revamp (#915).
* GOTO to C translator (#842)
* Linux Kernel Verification:
- simulation for Kernel user space copy (#1192).
- Mock kernel (#1135).
* Clang C++ Frontend:
- Improve code structure/ add new methods (#1189).
- Fix temporary object constructs for a single argument (#1196).
- Replaced throw with assert in string OM (#1163).
- Various fixes for C++ verification (#1138).
- Added CUDA and Qt/QtCore to include paths in CPP (#1131).
- Fix for TC template2 in 1108 (#1134).
- Embed CPP headers into ESBMC (#1124).
- Return a constant for MemberExpr to enumerator (#1119).
- Decouple TC20/36/39 from zero initialization (#1113).
- Fixed missing argument in copy constructor (#1112).
- Refactor/modify the COM (#1111).
- Fixed nested MemberExpr to struct/class method (#1102).
- Add TCs for CUDA OM (#1095).
- Fixed static member access (#1094).
- Fixed global initialization (#1086).
- Fixed inconsistent template specialization ids (#1079).
* SMT-backend:
- Fix usage of mk_ite by properly dispatching (#1201).
- More smtlib fixes (#1193).
- Fix symbol names and emission of AST node types in the smtlib backend (#1117).
- Restore some smtlib functionality with external solver (#1114).
- tuple-array-ast requires flattened array subtype in tuple-node-flattener (#1096).
* General Fixes:
- Fix intrinsic memset errors (#1199).
- Check for overflow during the generation of VLAs (#1190).
- Added an option to ignore strings (#1185).
- Only use custom limits.h for the old frontend; otherwise, clang provides its own for us (#1168).
- Restrict --unsigned-overflow-check to unsigned types only (#1143).
- Fixing arch for 32-bit arm analysis as armv6 (#1142).
- rename_type() should also recurse into operands (#1123).
- Bug fixing for printf return value (#1115).
- Add some more support for dynamic array sizes (#1101).
- Support dyn-off structures w/ array members from byte-arrays (#1090).
- Adjust also symbol's type and handle VLAs in adjust_type() (#1083).
- Opt into collecting types only for (some?) known irep annotations (#1077).
- Fix scanf bigint bug (#1076).
- Add support for malloc-scanf overflow checking (#1063).
- Fix overflow check for unsigned integer (#1058).
- Improve code coverage by modifing/adding assertions in GOTO (#1048).

*** Version 7.2
* Clang-C++ frontend:
  ** Added support for polymorphism (#919, #922, #923, #926, #927)
  ** Fixed crash regarding the definition of template functions in structs (#1045).
  ** Used value initialization for aggregate, including Plain Old Data (#1040).
  ** Fixed object composition, turning "this->itr = iterator()" into "iterator(&this->itr)" (#1007).
  ** Fixed various issues in our C++ operational models (e..g, #948, #995, #993, #988).
* Solidity frontend:
  ** Extended solidity-frontend to support Method Overload, Inheritance, and more return types for function calls (#1013).
  ** Added support for the solidity constructor and multiple contracts #949
  ** Fixed an error when calling a member function to get the Solidity return value (#1002).
* Operational models:
  ** Added overflow checks for the C functions scanf and fscanf (#976).
  ** Added model for aligned_alloc() via the combination of malloc and __ESBMC_assume on the address (#1035).
  ** Added lookup-based atoi, atol and atoll (#957, #958, #960, #1014, #1033).
  ** Optimize memset operations by initializing the entire object with the result of the C memset function (#640).
* Property Checking
  ** Added support for checking undefined behavior for shift operations  (#996, #1024).
  ** Added support for multiple property verification with three options: --multi-property, --multi-fail-fast, and  --parallel-solving (#1022).
  ** Added a color scheme when printing a message if a property has been successful or violated (#1022).
* Concurrency support:
  ** Added missing global variable information for a context switch (#1012).
  ** Fixed guard issues for multi-threaded goto programs (#974).
* Test case generation:
  ** Produce a test case in XML if a counterexample is found via the option --generate-testcase (#855).
* General fixes:
  ** Fixed the union used to generate doubles (Fix ieee_floatt to_double() #1038).
  ** Fixed access to multi-dim array members of unions (#1036).
  ** Added support for LLVM-16 compat (#1034).
  ** Made Z3 SMT formulas compatible with other solvers (#1023).
  ** ESBMC no longer throws errors for returning void expressions. (#1020).
  ** Improved bit mungling in the simplifier by adding a check that the operation can actually be performed meaningfully (#1019).
  ** Removed __ESBMC prefix when generating CE for intrinsic functions (#999).
  ** Do not call tuple_node_flattener for constant arrays of unions (#917).
  ** Fixed union initializer for cast-to-union cases supported by Clang and GCC (#1000).

*** Version 7.1
* Added an experimental flag to cache SSA assertions with `--cache-asserts` (SSA caching #827).
* Support for macOS M1 architecture (Fixed macOS M1 build #810).
* Additional operators for the goto-contractor with `--goto-contractor` (Goto contractor: support for multiple operators. #852).
* Interval analysis now supports integer and floating-point interval contraction for relational operators with `--interval-analysis` (Interval analysis fixes #861).
* Added `atexit` operational model (Atexit model implementation #859).
* Fixed an issue that caused extern variables to be linked incorrectly (Changes in the c_link and contextt to handle extern variables #881).
* The Clang C++ frontend now has support for the following features:
  ** single-inheritance (Single inheritance #882).
  ** multiple-inheritance (Multiple inheritance #884).
  ** arrow operator for objects (Method callsite via arrow operator #891).
* Various fixes (Fix returning instance of void #846, Fixed some warnings #860, [clang-c] fixed double type adjustment #866, Fix float cast #878, Fix union initializer type #904, [util] replace_symbolt learned to handle argumentt #907, Fix WinCI #911)  

*** Version 7
* Added support for GCC Vectors.
* Added support for the Jimple language.
* Added option to disable slicing on particular symbols, specified by annotation or on the command line (Support not slicing particular symbols #814).
* New C++ frontend now correctly handles new and delete ([clang-cpp-frontend] added support for new/delete #815) and references ([clang-cpp-frontend] Fix references #804).
* Fixed initialization of static storage compound literals ([clang-c-converter] fix initialization of static storage compound literals #816).
* Various fixes in old and new C++ frontends ([clang-c*-frontend] Minor fixes #808, [cpp] Fixed zombie operand #811, [cpp] quick fix for more zombie codet operand #839).
* Various bugfixes in the --goto-contractor option (#836).

*** Version 6.10
* Lots of bugs related to unions have been fixed.
* Compound Literals are now supported.
* _ExtInt struct fields now have proper padding and alignment.
* A bug where the size of 3-dimensional arrays was not being computed correctly has been solved.
* A new intrinsic for stack allocation has been added: __ESBMC_alloca.
* The Solidity frontend now has support for: bool literal and while.
* The clang-cpp-frontend now has support for: CXXThisExpr and CXXConstructor.
* New options have been added: --file-output, --cex-output, --initialize-nondet-variables, and --non-supported-models-as-zero.
* A new experimental optimization for intervals contraction was added: --goto-contractor. More details about this optimization at: https://arxiv.org/pdf/2012.11245.pdf. 

*** Version 6.9
* Fixed a bug where Z3 bv were not encoded correctly for signed numbers.
* Improved counterexample line numbering.
* Improvements over concurrency checks.
* Bug fixes.

*** Version 6.8
* ARM Release!
* Solidity Support!
* Value set analysis.
* New message system.
* Bounded goto unroll algorithm.

*** Version 6.7
* Memory Model allignment improvements.
* Added a new option for compact-trace (--compact-trace).
* Added support for gcc's Cast to Union extension.
* Windows Release (Z3 only).

*** Version 6.6
* Fix parallel k-induction verification.
* Removed incremental context bound options.

*** Version 6.5
* Initial C++ clang frontend.
* Added new option for incremental context bound verification.
* Added support for _ExtInt to create custom sized bitvectors.
* Several fixes and improvements to our libc models.
* Fix infinite loop when verifying recursive programs with k-induction.
* Update clang to 11.0.
* Several minor bug fixes.

*** Version 6.4
* Refactored concurrency to check global writes in arrays.
* Removed python API from ESBMC.
* Updated CVC4 build instructions.
* Fixed pointer arithmetic in the dereference module.
* Added models for cond_broadcast and mutex_destroy.
* Rename test cases that give trouble in Windows.
* Added models for key_create, getspecific, and setspecific.

*** Version 6.3
* Stack property verification support.
* ESBMC now supports Microsoft extensions.
* -f an -W flags are forwarded into clang.
* Float models refactoring, which enabled macOS CI..
* Fixed issue that caused a deref violation in VLAs.
* Union bitfields no longer throws a segfault.
* Unary sideeffects are handled properly.
* CVC4 enconding for FPs is fixed.

*** Version 6.2
* Cmake is now the default build system.
* ESBMC now defaults to 64 bits mode.
* ESBMC now defaults to use floating-points.
* Updated ESBMC to use clang version to 9.0 minimal.
* Updated ESBMC to use Boolector 3.2.
* Updated Z3 and boolector licenses.
* Simplified some methods in our SMT conversion API.
* Removed goto-unwind option.
* Removed duplicated Z3 header.
* Removed unnecessary code due to new c++ standards.
* Removed unnecessary mp_integer typedef.
* Removed old regressions.
* Removed autotools.
* Added support for Float128 in the frontend.
* Several expression optimizations implemented.
* Several new cex queries implemented.
* Fixed several small issues in all SMT backends.
* Fixed alloca'd variables not being destroyed at the end of frames.
* Fixed some variables going out of scope but not being marked as detroyed.

*** Version 6.1
* Use clang to generate declaration names.
* Added support for popcount.
* Added support for bswap.
* Added support for __auto_type.
* Added support for atomic types.
* Added support for atomic expressions.
* Added support for Boolector 3.0.
* Update clang headers to 7.0.
* Update Z3 header to 4.8.0.
* Fix ESBMC not reporting bugs when accessing variables that went out of scope.
* Several minor bug fixes.

*** Version 6.0
* New bidirectional k-induction algorithm (bkind).
* New invariant generator based on intervals from CPROVER.
* Improvements to constraint generation in the k-induction algorithm.
* Fix hash calculation for floats.
* Fix missing typecasts for shift operations.
* Fix correctness witnesses not being generated.

*** Version 5.1
* Backported fixes to the floating-point API from Z3 4.7.1.
* Fixed compilation with clang.
* Fixed wrong integer division simplification.
* Fixed infinite loop reported in #7.

*** Version 5.0
* Massive update to the SMT backend:
  - New floating-point API, supporting all solvers (based on Z3).
  - Improved AST and Sort wrappers.
  - Improved solver wrappers (now with pre-condition checks).
  - Removed variadic method to create sorts.
  - Removed ID based method to create ASTs.
* Improved support for memset with constant size.
* Fixed a number of wrong optimizations.
* Fixed cex generation for arrays.
* Fix model generation in MacOS.
* Update APIs for Z3 4.6, MathSAT 5.5.2 and clang 6.0.0.
* Applied clang-format in the whole code base.

*** Version 4.6
* New support for bitfield verification.
* New option to slice assumes.
* New option to check termination.
* New floating-point API in the backend.
* Improvements to cex and witness generation.
* Removed a lot of dead code.

*** Version 4.5
* We use clang to generate tag names now.
* General improvements to SSA generation.
* Fix alignof evaluation by clang.
* Fix cex generation of structs.
* Fix VLA encoding of structs.
* Fix statement expressions generating out of order instructions.
* Removed a lot of dead code.

*** Version 4.4.1
* Remove option to disable clang.
* Improvements to ax_clang to support Ubuntu/Debian/Fedora.
* Fix struct/union symbol dump.
* Fix a number of status messages.
* Fix cex when using z3 in fp mode.
* Fix old c++ frontend not finding a program entry point.

*** Version 4.4
* Fix crash with --smt-during-symex due to equations being shared_ptr.
* Fix a double increment when encoding tuples.
* Fix crash when building ESBMC with an assertions enabled clang build.
* Fix a bug when trying to verify a program with a free(NULL) statement.
* New --ssa-* options to add information and/or change SSA printing format.
* A number of improvements to the code base thanks to clang-tidy.
* Improved clang detection in autotools.

*** Version 4.3
* New support to encode square root operations using fp.sqrt.
* Improvements to cex generation.
* Improvements to status messages.
* Clang is now the default frontend.
* Fix VLA bounds check.
* Fix verification of programs with envp.
* Fix wrong message when using __ESBMC_assert.
* Fix wrong index generation when using multidimensional arrays.

*** Version 4.2.1
+ Fix bug when inlining functions and esbmc would assume that.
the variables from the inlined function were global.
+ Fix python compilation on MacOS.

*** Version 4.2
+ Full support for va_args.
+ Dropped openssl dependency.
+ Update clang headers to clang 4.0.
+ Cleanup ESBMC options.
+ Fix build on MacOS.
+ Fix creation of multidimensional arrays.

*** Version 4.1
+ Support for Boolector 2.4.1.
+ Fix static libesbmc not being built.
+ Fix a static initialization order fiasco.
+ Removed the need for ac_config.h when using libesbmc.

*** Version 4.0
+ 100% more python: new python API for faster prototyping.
+ Support to build ESBMC as library.
+ Improved guards generation: greatly decrease in memory usage.
+ Fix support for addition, subtraction and multiplication for
  MathSAT, when running in integer/real mode (no division for now).
+ Memory leak fixes in a number of places.
+ General bug fixes.

*** Version 3.2
+ Support for integer/real arithmetic when using MathSAT.
+ New option to dump the SMT formula (only Z3).
+ Partial support for va_args.

*** Version 3.1
+ Rewritten k-induction (should greatly reduce false positives).
+ Support for floating point with Z3 and Mathsat (use --floatbv).
+ Improved witness generation (no need for tokenizer anymore).
+ Correctness witness generation.
+ Shipping with Mathsat 5.3.14, Z3 4.5.0 and Boolector 2.2.0.
+ General bug fixes.

*** Version 3.0.2
+ Fix bug on deadlock verification.
+ Fix an off-by-allthenumbers when dealing with dynamic structs.
+ Fix compilation with newer version of GCC.
+ Updates to support clang 3.9.0 on our frontend.
+ We now ship with all clang 3.9.0 headers.

*** Version 3.0.1
+ Fix falsification crash.
+ Fix switch condition typecast.
+ Fix float literal generation.
+ Back to Z3 v4.4.1 (stable API).
+ Update to Boolector v2.2.0.

*** Version 3.0.0
+ Several bugfixes.
+ New clang frontend!
+ Update Z3 to v4.4.2 (commit 0870b4a5).
+ Update Boolector to v2.1.1.

*** Version 2.1.0
+ Several bugfixes.
+ New option to fully inline a program.
+ New option to unwind loops at goto level.

*** Version 2.0.0
+ Released ESBMC open source at https://github.com/esbmc/esbmc.
+ Build with autoconf.
+ Adjust union implementation: because SMT does not have a good way of.
  representing unions, we now allocate a byte array as storage for unions, and
  force all union accesses to be performed through pointers. The dereference
  layer handles the decomposition of these accesses to byte array accesses.
  This seems to work well; the only limitation is that assignments of type
  union become assignments of type array, which the dereference layer can't
  handle. This will be fixed in a future release.
+ Support assignments with structure type better, and dereferences that
  evaluate to a structure.
+ Fix a number of byte-order inaccuracies. The "byte_extract" and update ireps
  will now only operate on scalars; the pointer layer handles all other.
  circumstances where the byte model representation is required
- For this release, K-Induction support is disabled. Please use a previous
  version for kinduction.

*** Version 1.25
+ Bugfixes for the k-induction implementation.
+ Boolector is now the default solver.
+ Improved the C++ parser and template.
+ Decreased memory usage.

*** Version 1.23
+ Bugfixes for the k-induction implementation.
+ Added the ability to run each step of the k-induction process concurrently.
  --k-induction-parallel will run the base, forward condition, and inductive
  step in separate concurrent subprocesses.

*** Version 1.22
TACAS14 competition release.
+ Substantially altered the memory model. The majority of dereferencing logic
  now occurs while the SSA program is produced (and thus is visible in
  --program-only), rather than at the solver level.
+ Unaligned dereferences will now produce an assertion failure; disable them
  with --no-align-check.
+ Expunged a large variety amount of the stringly-typed internal representation
+ Updated Z3 api to 4.0, to use their reference counting approach and new
  solver API. We recommend using Z3 4.0 itself, as later versions seem to
  exhibit a performance regression.

*** Version 1.21.1
+ Fixed an option-passing failure present in 1.21, that led to K-induction
+ not operating correclty.

*** Version 1.21
+ Enhance support for C++ model checking.
+ Switch LTL modelling to support checking multiple property truth values.
+ Fixed a pointer-tracking error breaking some leaked-memory detection tests.

*** Version 1.20 ***
TACAS13 competition release.

*** Version 1.19 ***
Date 20/06/2012
+ Support more of the pthreads library (pthread_join).
+ Fix an issue with guards not being shared between threads.
  - Under certain circumstances, a condition guarding a visible instruction is
    not applied to other threads after a context switch, leading to impossible
    counterexamples.
+ Fixed a problem where some dynamically allocated objects allocation status
  became incorrect.

*** Version 1.18 ***
Date 19/01/2012
+ Internal efficiency improvements.
+ Fixed many pointer model errors encountered during TACAS 2012.
+ Binaries for running on MS Windows (MinGW).

*** Version 1.17 ***
Date 15/10/2011
+ Release for TACAS 2012 Software Verification competition.
+ Numerous minor bug fixes related to the Z3 solver backend.

*** Version 1.16 ***
Date: 10/05/2011
+ New Feature
 - Support for state hashing to reduce the number of redundant interleavings.
+ Enhancements
 - Minor bug fixes related to the C enumeration, code location ordering and
   memory leaks.

*** Version 1.15.1 ***
Date: 18/01/2011
+ Enhancements
 - Minor bug fixes related to data race detection of arrays and the
   counterexample beautification;

*** Version 1.15 ***
Date: 17/01/2011
+ Enhancements
 - Implementation of constant propagation for arrays, structs and unions.
 - Minor bug fixes in the front-end;

*** Version 1.14 ***
Date: 15/12/2010
+ Enhancements
 - Minor bug fixes related to the integer and real arithmetic encoding;
 - Implementation of some optimization to improve the performance
   during the loop unwinding.

*** Version 1.13 ***
Date: 23/11/2010
+ Enhancements
 - Fixed one bug related to the SMT encoding of arrays that contain
   structs reported by Jeremy;
 - Integration of a new version of the SMT solver Z3 (i.e., v2.13).

*** Version 1.12 ***
Date: 08/11/2010
+ New Feature
 - Output verification conditions into the SMT-lib logics QF_AUFBV
   and QF_AUFLIRA (use the option --qf_aufbv or qf_auflira followed by
   --outfile file.smt).
+ Enhancements
 - Minor bug fixes related to the ANSI-C front-end and dynamic memory allocation.

*** Version 1.11 ***
Date: 18/10/2010
+ New Features
 - Preliminary support for detecting memory leaks.

*** Version 1.10 ***
Date: 13/10/2010
+ New Feature
 - Support for static partial order reduction (use the
   option --no-por to disable it);
+ Enhancements
 - Fixed one bug related to context-switch before array updates;
 - Fixed one bug related to pointer typecast reported by Jie Gao.

*** Version 1.9 ***
Date: 17/09/2010
+ New Feature
 - Support for checking atomicity violation at visible statements
   (use the option --atomicity-check).

*** Version 1.8 ***
Date: 06/09/2010
+ Enhancements
 - Included an option --control-flow-test to allow context switch before
   control flow tests;
 - Integration of a new version of the SMT solver Z3 (i.e., v2.11).
+ Known Issues
 - We do not add data race checks for structs and pointers.

*** Version 1.7.1 ***
Date: 26/07/2010
+ Enhancements
 - Fixed one bug reported by Jie Gao related to dynamic memory allocation.
+ Known Issues
 - We do not add data race checks for structs and pointers.

*** Version 1.7 ***
Date: 22/07/2010
+ Enhancements
 - Fixed two bugs reported by Jie Gao related to atomicity violation
   and condition checking of "for" loops;
 - Fixed a bug related to function pointers;
 - Integration of a new version of the SMT solver Z3 (i.e., v2.8).
+ Known Issues
 - We do not add data race checks for structs and pointers.

*** Version 1.6 ***
Date: 03/06/2010
+ Enhancements
 - Integration of a new version of the SMT solver Z3 (v2.7);
 - The UW procedure is able to find deadlocks.
+ Known Issues
 - We do not add data race checks for pointers (i.e., we miss data race
   bugs originated from pointers).

*** Version 1.5 ***
Date: 14/05/2010
+ New Features
 - Support for data race detection (use the option --data-races-detection).
+ Enhancements
 - Improved the command-line interface: (i) we provide more details about the
   UW algorithm in the console and (ii) we also allow the user to disable the
   deadlock detection through the command line (thus simplifying the formula
   to be sent to the SMT solver);
 - Minor bug fixes related to the pthread_join function and the UW procedure
   (now we can support thousands of control literals).
+ Known Issues
 - We do not add deadlock assertions to be checked using the UW procedure;
 - We do not add data race assertions for pointers (i.e., we miss data race
   bugs originating from pointers).

*** Version 1.4.1 ***
Date: 10/05/2010
+ Enhancements
 - Minor bug fixes related to the concurrency stuffs.
 - Integration of a new version of the SMT solver Z3 (v2.6).
+ Known Issues
 - The UW procedure does not work for multi-threaded C programs that require
   more than 500 control literals.

*** Version 1.4 ***
Date: 25/04/2010
+ New Features
 - Support for context-bounded model checking (use option --context-switch nr);
 - Support for detecting the potential for deadlock;
 - Detection of abandoned locks;
 - Detection of lost signals;
 - Support for creating dynamically threads, mutexes, and condition variables.
+ Known Issues
 - The UW procedure does not work for multi-threaded C programs that require
   more than 500 control literals.

*** Version 1.3.2 ***
Date: 08/04/2010
+ Enhancements
 - Minor bug fixes related to concurrency reported by Byron Cook.

*** Version: 1.3.1 ***
Date: 29/03/2010
+ Enhancements
 - Minor bug fixes related to dynamic memory allocation;
 - Improvement in the command-line interface;
 - Integration of a new version of the SMT solver Z3 (v2.5).

*** Version: 1.3 ***
Date: 13/03/2010
+ New features:
 - Lazy exploration of the threads interleavings;
 - Generate one single formula using the schedule recording approach to verify multi-threaded programs;
 - Generate underapproximation and widening models for the multi-threaded programs;
 - Support for concurrent C programs with shared memory;
 - Support for synchronization primitives with mutexes and conditions;
 - Detection of global deadlock with mutexes and conditions;
 - Additional support for atomic sections through the functions __ESBMC_atomic_begin() and __ESBMC_atomic_end().

