You're right. I've been using --use-forked-stp all the time, but it turns out that --with-stp-server switches the base solver from STPSolver to STPServerSolver, which doesn't respect --use-forked-stp. Making STPServerSolver respect the option and forking seems to be the best solution.
Thank you! Dawson Engler wrote: > Maybe I'm misunderstanding something --- can't you just run STP as a > forked process? That seems like it would solve your issue. > >> I have been encountering stack overflow in STP, which is caused by >> function calls more than 6000 levels deep. The functions include >> BEEV::ASTNode::LetizeNode and BEEV::BeevMgr::TermToConstTermUsingModel, >> calling themselves, respectively. >> >> At least in one case I observed that it was not a bug in the logic >> but a very complex query that could be causing the problem. >> >> The stack overflow manifests itself in the form of segmentation faults, >> which I cannot "catch" in the program like a C++ exception. When this >> happens, everything stops and I lose valuable states that have not >> finished and produced test cases. I could use a signal handler, but >> that would handle all segfaults, and I'm not sure if it's a good idea. >> >> Do you have any good ideas? -- Seungbeom Kim
