search

gipsyh / rIC3

A high-performance implementation of the IC3/PDR algorithm in Rust.
GNU General Public License v3.0
19 stars 2 forks source link

Claims safe for unsafe instance. #5

Open Froleyks opened 1 week ago

Froleyks commented 1 week ago

The bug.btor2 instance is clearly unsafe as the uninitialized oracle may be 1. The bug is presumably in the bit-blasting.

Also I consider result: true to be confusing. I suggest printing result: safe / result: unsafe

~/c/m/r/t/release ⌂ cat bug.btor2 1 sort bitvec 1 2 state 1 oracle 3 state 1 latch 4 init 1 3 2 5 next 1 3 3 6 bad 3 ~/c/m/r/t/release ⌂ ./btormc bug.btor2 sat b0

0

0 1 oracle#0 @0 . ~/c/m/r/t/release ⌂ ./rIC3 bug.btor2 the model to be checked: bug.btor2 best configuration: ic3 --ic3-inn result: true ~/c/m/r/t/release ⌂ ./rIC3 --version rIC3 1.1.0 branch:master commit_hash:eb12120e build_time:2024-11-19 14:05:04 +01:00 build_env:rustc 1.84.0-nightly (03ee48451 2024-11-18),nightly-x86_64-unknown-linux-gnu

gipsyh commented 1 week ago

I fixed it in the latest commit, as it was caused by a bug in btor2aiger.