Closed quickbeam123 closed 3 months ago
Stack overflow in Term::toString
, which calls TermList::asArgsToString
, which calls Term::toString
.
I don't really see why we should need toString
very often versus an ostream
-based solution. I'll rewrite this function and make it stream-y in the meantime.
There is also a problem that the function (by mistake, I think) prefers the recursion path instead of the explicit-stack based one. So nothing against stream-based outputting, but the one-liner from https://github.com/vprover/vampire/pull/569 should be a fix for this particular case...
Try
./vampire Problems/SYN/SYN986+1.004.p
. Looks like this on my computer: