draperlaboratory/cbat_tools

Refuted goals not showing when checking loop invariants

Opened this issue 3 years ago · 0 comments

fortunac commented 3 years ago

Currently when running

https://github.com/draperlaboratory/cbat_tools/blob/ccasin/invariant-example/wp/resources/sample_binaries/loop_invariant/sum_array/run_wp.sh

with the --show=paths flag, we return SAT but have no refuted goals.