search

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

Refuted goals not showing when checking loop invariants #323

Open fortunac opened 3 years ago

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.