Known Solver Issues

November 17, 2020 ยท View on GitHub

Princess

  • Princess is recursive and might require a large amount of stack memory. If you experience stack overflows or Princess returns OutOfMemory, try increasing the stack size with the JVM parameter -Xss.
  • Requesting termination via the ShutdownNotifier works only in limited circumstances.

SMTInterpol

  • SMTInterpol does not support multiple concurrent stacks under the same context.

CVC4

  • Our version of CVC4 does not support any garbage collection in the native library. This might cause memory leaks.

MathSAT (on Windows)