Look into performance issues with large unrolls about pono HOT 8 CLOSED

I get the following message when I try to reproduce

time ./cosa2  -k 26000 example/example.btor2 
Name has already been used.
unknown
b0

real	0m0.847s
user	0m0.438s
sys	0m0.409s

from pono.

Hmm that’s interesting. I was just using it through the API, not the command line. I’m not sure why that’d be any different though. I can look into it.

from pono.

Fixed in master -- that file reuses symbols for btor lines

from pono.

so, is there still the issue?

from pono.

Oh yeah the issue is still there. I only fixed the Name issue, I didn’t look into the unroller at all. By the way, I don't know if the performance issue is in cosa2 or smt-switch.

from pono.

if you have the test case, I would like to also look into it.

from pono.

Here's a test that just unrolls it -- takes about 4.5 minutes on my desktop. There's a Makefile that should work for you out of the box. Just needs to be in the top level of the cosa2 repository and have smt-switch already built in the usual place and cosa2 built. Then run ./test-unroller.out.
test-unroller.tar.gz

from pono.

Closing this, as the current version of Pono (d5f968d) solves the example in under 5s.

from pono.