search

boogie-org / corral

solver for the reachability modulo theories problem
MIT License
58 stars 29 forks source link

Internal bug: Refinement unable to make progress #125

Open unboxedtype opened 4 years ago

unboxedtype commented 4 years ago

Hi!

Running Corral on a Boogie program gives the following:

$ corral /z3opt:smt.bv.enable_int2bv=true /useArrayTheory /recursionBound:5 ./minidao.bpl 
Corral program verifier version 1.0.12.0
Single threaded program detected
Verifying program while tracking: {assertsPassed}
Program has a potential bug: False bug
Verifying program while tracking: {assertsPassed, voted_yes, voted_no}
Program has a potential bug: False bug
Verifying program while tracking: {assertsPassed, voted_yes, voted_no, now, proposal_deadline}
Program has a potential bug: False bug
Verifying program while tracking: {assertsPassed, voted_yes, voted_no, now, proposal_deadline, DAO_balance}
Program has a potential bug: False bug
Verifying program while tracking: {assertsPassed, voted_yes, voted_no, now, proposal_deadline, DAO_balance, msg_sender}
Program has a potential bug: False bug

**Error, internal bug: Refinement unable to make progress**

After several refinement steps, it fails to progress further. Do you have any clues regarding why this happens and what can I do about it? Inside my program, I use bv2int, int2bv, quantifier constructs: might this be a reason for this?

I do not have a minimal reproducing sample, and not sure if attaching the full source code is a good idea.

Thanks!

akashlal commented 4 years ago

@unboxedtype This error happens due to incompleteness from the SMT solver. Corral was unable to find additional variables to track so as to rule out the last false counterexample. The incompleteness usually is from quantifiers that are not well-behaved (without good triggers). Try to identify these quantifiers and see if you can remove them (use a loop instead) or add triggers.

Another option is to use the flag /trackAllVars. In this case, the incompleteness can still show up, but instead of this internal bug, corral may report a false bug.

unboxedtype commented 4 years ago

I removed bv2int, int2bv, quantifiers over integers. I changed all integers to bitvectors, and quantify only over thin bitvectors, so now its working, I am good!

Thanks!

P.S. It might be a good idea to enhance the error message to give a clue for a poor soul.