Skip to content
This repository has been archived by the owner on Aug 23, 2024. It is now read-only.

Witness for second bad claims to be witness for both #89

Closed
nakengelhardt opened this issue Mar 25, 2020 · 2 comments
Closed

Witness for second bad claims to be witness for both #89

nakengelhardt opened this issue Mar 25, 2020 · 2 comments

Comments

@nakengelhardt
Copy link
Contributor

The attached design contains two bads: design_btor.btor.txt

Running btormc design_btor.btor.txt accordingly produces two witnesses: design_btor.wit1.txt and design_btor.wit2.txt

The first witness is a witness for b0 and works correctly:

> btorsim design_btor.btor.txt design_btor.wit1.txt
.

The second however claims to be a witness for b0 b1 but is actually only a witness for b1:

> btorsim design_btor.btor.txt design_btor.wit2.txt
.
*** 'btorsim' error: claimed bad state property 'b0' id 25 not reached
@mpreiner
Copy link
Member

Thanks Nina! Fixed with 9a13228 on master.

@nakengelhardt
Copy link
Contributor Author

Excellent! Now I have boolector for cover mode working in SymbiYosys 🎉

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants