Release Notes of the ESBMC model checker

*** 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().

