Missing refuted goals

[ccasin]

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 0c20040) 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?