rIC3 achieved first place in both the bit-level track and the word-level bit-vector track at the 2024 and 2025 Hardware Model Checking Competition (HWMCC).

To view the submission for HWMCC'24, please checkout the HWMCC24 branch or download the binary release at https://github.com/gipsyh/rIC3-HWMCC24.

• [CAV2025] The rIC3 Hardware Model Checker
• [CAV2025] Deeply Optimizing the SAT Solver for the IC3 Algorithm
• [DAC2024] Predicting Lemmas in Generalization of IC3
• [arXiv] Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3

cargo install rIC3

rIC3 can be compiled on both Linux and macOS.

• Install the Rust compiler https://www.rust-lang.org/
• git clone --recurse-submodules https://github.com/gipsyh/rIC3
• Install gmp and mpfr required by Bitwuzla apt install libgmp-dev libmpfr-dev or brew install gmp mpfr
• Build cd rIC3 && cargo b --release
• Run cargo r --release -- check <AIGER/BTOR> portfolio
• Install cargo install --path .

• 16-threads Portfolio ric3 check <AIGER/BTOR> portfolio
• single-thread IC3 ric3 check <AIGER/BTOR> ic3

• build image: docker build -t ric3 .
• run: docker run -v <AIGER/BTOR>:/model.<aig/btor> ric3 check model.<aig/btor> portfolio

Copyright (C) 2023 - Present, Yuheng Su (gipsyh.icu@gmail.com). All rights reserved.