epfl-lara/leon — pull request #63 by samarion (2014-09-10 16:58:19+00:00)
Title: Updated unrolling solver to work with UninterpretedZ3Solver

UnrollingSolver with UninterpretedZ3Solver not as powerful as FairZ3Solver. Running

./leon src/test/resources/regression/verification/purescala/valid/AmortizedQueue.java

will not terminate whereas it takes only a few milliseconds using the FairZ3Solver. I don't really see how unrolling more could keep the UnrollingSolver from getting the right proof...