update

Cargo.toml

@@ -20,7 +20,6 @@ logic-form = { path = "./deps/logic-form", version = "0.2.6" }
 giputils = { path = "./deps/giputils", version = "0.2.3" }
 satif = { path = "./deps/satif", version = "0.1" }
 abc-rs = { path = "./deps/abc-rs", version = "0.2" }
-btor = { path = "./deps/btor-rs", version = "0.1" }
 clap = { version = "4.5.16", features = ["derive"] }
 rand = "0.8.5"
 ctrlc = { version = "3.4.1", features = ["termination"] }

src/main.rs

@@ -1,7 +1,6 @@
 #![feature(ptr_metadata)]
 
 use aig::Aig;
-use btor::btor_to_aiger;
 use clap::Parser;
 use rIC3::{
     bmc::BMC,
@@ -29,9 +28,7 @@ fn main() {
         println!("the model to be checked: {}", options.model);
     }
     let mut aig = if options.model.ends_with(".btor") || options.model.ends_with(".btor2") {
-        options.certifaiger_path = None;
-        options.certify = false;
-        btor_to_aiger(&options.model)
+        panic!("rIC3 currently does not support parsing BTOR2 files. Please use btor2aiger (https://github.com/hwmcc/btor2tools) to first convert them to AIG format.")
     } else {
         Aig::from_file(&options.model)
     };