Key Information About the Vulnerability Issue Title: [Bug] Heap-buffer-overflow in Minisat::Solver::value #55 Vulnerability Type: Heap-buffer-overflow Target: MiniSat Description The vulnerability is triggered when parsing a crafted DIMACS file containing a large variable index, such as 2147483648. This leads to integer overflow or signedness issue, causing a negative index access (buffer underflow) in . Environment OS: Linux x86_64 Compiler: Clang Build Configuration: Release mode with ASan enabled Vulnerability Details Target: MiniSat Vulnerability Type: CWE-125: Out-of-bounds Read (Underflow) / CWE-190: Integer Overflow Function: Minisat::lbool::operator^ (called by Solver::value) Location: core/SolverTypes.h:105 (and core/Solver.h:351) Root Cause Analysis: The PoC contains a value that exceeds INT_MAX (2^31 - 1). When MiniSat processes this value, it results in heap buffer underflow due to negative index access in the array. Reproduce 1. Build MiniSat with Release optimization and ASAN enabled. 2. Run with the provided PoC file using the command: ASAN Report The ASAN report confirms a read violation 1 byte before an allocated heap region, indicating heap buffer underflow. Related CVE CVE-2026-2644 is associated with this issue.