search

mgudemann / iimc

Other
11 stars 6 forks source link

SIGSEV when using the --print_cex option flag #6

Open kavehshamsi opened 6 years ago

kavehshamsi commented 6 years ago

iimc examples/ctl/palu.aig --ctl examples/ctl/palu.ctl --print_cex --iictl_verbosity 3 --pi 0 will give you a segment fault. Tried the --print_cex flag on numerous aigs and ctls all end up with the same issue.

mgudemann commented 6 years ago

@kavehshamsi thanks for reporting this. Please note that I am not a maintainer of iimc, I keep this repo more or less for myself (and for others) as the original site is unavailable since a while

My guess is that AIGER cex for CTL are not supported, so a solution would be to ignore/warn when using --print_cex which the iictl tactic.

If you require this, I am happy to accept PRs, though. Else you might want to get in touch with the original authors.

kavehshamsi commented 6 years ago

@mgudemann thanks for the response. I will try to see if I can solve it and make a PR. Bests :)

mgudemann commented 6 years ago

@kavehshamsi sounds good.

Out of curiosity, is there a common format for CTL CEX ? It seems that HWMCC only wants witnesses for SINGLE, safety properties.