Given a btor2 circuit, we now have a concise way to generate a counter example, using SeaHorn, and construct a valid witness for the original btor2 circuit.
The docker file and ./get_cex_seahorn files capture the necessary details of how this is done.
Given a
btor2circuit, we now have a concise way to generate a counter example, usingSeaHorn, and construct a valid witness for the originalbtor2circuit.The docker file and ./get_cex_seahorn files capture the necessary details of how this is done.