AV: Blowup for multi arity maps

boogie-org / corral

solver for the reachability modulo theories problem

MIT License

58 stars 29 forks source link

AV: Blowup for multi arity maps #61

Open shuvendu-lahiri opened 6 years ago

shuvendu-lahiri commented 6 years ago

For the example:

AngelicVerifierNull.exe testInst.bpl /nodup /traceSlicing /copt:recursionBound:5 /copt:k:1 /copt:tryCTrace /EE:noFilters /EE:onlyDisplayAliasingInPre- /SDV

causes AV to blowup due to the multi arity maps.

Need to simplify the case splits that are clearly false [example])https://github.com/boogie-org/corral/blob/master/AddOns/AngelicVerifierNull/test/c%23/tinybct_samples/testInst.bpl)

zvonimir commented 4 years ago

I am guessing nobody will work on this any time soon, if ever. @shuvendu-lahiri and @akashlal : are you ok if I mark this as "won't fix" and close the issue?