search

ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49 stars 43 forks source link

IMC vs. RIMC finds loops at different times #319

Closed leventeBajczi closed 1 week ago

leventeBajczi commented 2 weeks ago

sv-benchmarks/c/hardware-verification-bv/btor2c-lazyMod.h_Spinner.c behaves differently with IMC and RIMC:

SV-COMP25_unreach-call-IMC-Z3.btor2c-lazyMod.h_Spinner.yml.log

SV-COMP25_unreach-call-RIMC-Z3.btor2c-lazyMod.h_Spinner.yml.log

leventeBajczi commented 2 weeks ago

The problem seems to be that in the reversed case, we can prove that the loop-free state space can be explored without having to interpolate.