The paper introduces a tool for formally verifying ANSI-C programs using Bounded Model Checking (BMC). The tool supports a wide range of ANSI-C features, including pointer constructs, dynamic memory allocation, recursion, and floating-point types. It is designed to be highly automated, with the user only needing to specify the BMC bound. The tool includes a graphical user interface (GUI) that allows users to step through counterexample traces, similar to a debugger, making it accessible to non-expert users. The tool can also compare an ANSI-C program with a Verilog design, ensuring consistency between the two implementations. The paper details the process of generating bit-vector equations from the ANSI-C program and converting them to Conjunctive Normal Form (CNF) for SAT solving. The tool is available for Linux, Windows, and Solaris, with detailed documentation and a tutorial.The paper introduces a tool for formally verifying ANSI-C programs using Bounded Model Checking (BMC). The tool supports a wide range of ANSI-C features, including pointer constructs, dynamic memory allocation, recursion, and floating-point types. It is designed to be highly automated, with the user only needing to specify the BMC bound. The tool includes a graphical user interface (GUI) that allows users to step through counterexample traces, similar to a debugger, making it accessible to non-expert users. The tool can also compare an ANSI-C program with a Verilog design, ensuring consistency between the two implementations. The paper details the process of generating bit-vector equations from the ANSI-C program and converting them to Conjunctive Normal Form (CNF) for SAT solving. The tool is available for Linux, Windows, and Solaris, with detailed documentation and a tutorial.