AV: EE scalability issue

boogie-org / corral

solver for the reachability modulo theories problem

MIT License

58 stars 29 forks source link

AV: EE scalability issue #37

Open shaobo-he opened 7 years ago

shaobo-he commented 7 years ago

For the attached bpl file, EE times out three times on my machine. One of them does in TryRewriteITE and the rest two in ComputePre. hinst.zip

To reproduce, try avn hinst.bpl /sdv /blockOnFreeVars /timeoutEE:200 /timeout:1000 /noEbasic /EE:ignoreAllAssumes+ /dontGeneralize /dumpResults:results.txt /EE:onlySlicAssumes+ /EE:ignoreAllAssumes- /killAfter:3600

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?