search

draperlaboratory / cbat_tools

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

Missing refuted goals #341

Open ccasin opened 3 years ago

ccasin commented 3 years ago

Sometimes when using --show=paths or --show=refuted-goals, wp fails to find a refuted goal. Our examples at the moment all involve loop invariants.

I have pushed a branch where I see this behavior:

https://github.com/draperlaboratory/cbat_tools/tree/ccasin/missing-goal

Running run_wp.sh in wp/resources/sample_binaries/loop_invariant/sum_array gives me the following output:

missing-goal-output.txt

The only change I've made to fortunac/loop-invariant-testing (commit 0c2004017f2b8eee2af1fc03934a4a442e821b9b) is that I added a precondition:

(assert
   (and (= init_RDI #x0000000000000001)
        (= init_RSI #x4000000000000000)))

@fortunac Can you see if you can reproduce when you have a minute?