We've built a tool using LD_PRELOAD that speeds up SAT and QBF solvers (but the same idea could be used to speed up other programs too). The idea is to fork, then LD_PRELOAD the other program and overwrite its read functions (and equivalents to also capture inlined read functions). The child process loads some solver which will try to read its input from STDIN. The overwritten read is triggered and instead of just reading, our library shim connects to the parent process. The parent process feeds the child with data, the shim converting the data into text, feeding it to the solver as if it would be reading from a file. Now once we are finished with stating the problem and want to query it (i.e. send assumptions, in QBF or SAT solver speech), we issue a fork command, which lets the child process fork again into a second process, while the solver program thinks it is still in the read() call. We then feed the assumptions only to this grandchild, close its STDIN, and return the result to the calling parent process. When there's another assumption, we can issue the fork again and send assumptions to the new instance, never having to process the full problem again This is nice when the formula is large and the assumptions are small and numerous, which (e.g. for parallelization) was very useful in our research. The copy on write nature of fork() of course also helps, effectively reducing the required RAM to keep solvers in memory. The best of all this, it works remarkably well on Linux and is even (mostly) POSIX conforming! Check out our paper: https://ceur-ws.org/Vol-3201/paper1.pdf Or just the code: https://github.com/maximaximal/quapi