Andrew V. Teylu

You need to build CryptoMiniSat with `-DLARGEMEM:BOOL=ON` when you call its CMake. Once you've build CMS with `-DLARGEMEM:BOOL=ON`, you then build STP "normally" (but linking against your large-mem-enabled CMS).

> However, the result of solve SAT model can't map back SMT model yet. So STP does this *internally* (e.g., that's how it is able to generate a model on...

> Maybe this instance is hard to solve(24 hour in 5 threads), some easy instances not Aborted. Ah, okay, so it _could_ be a memory issue then, if things take...

Just so we know, are you saying that: - 93f7f2d40ee1b951b645cd7e8b6fcb2387b27b67 works (== 0.05 seconds) - 7b05982b2157bfa30595c8ebf6b83b3fd3fb2f16 doesn't work (>= 3 hours) ? If you already know the commit hash that...

Given the error message: maybe a missing `__init__.py` in the build folder? When you do something like `cmake --install .`, I imagine this puts the `stp` folder into `site-packages`; however,...

MiniSat and CMS are dependencies of STP; they should be installed by doing `cmake --install .` in the build folder of the dependency rather than STP’s build. To be honest:...

Are you on Apple silicon? What version of macOS? (I have access to an M1, but not until next week)

As a note for something not in the description: there are other uses of `PYTHON_EXECUTABLE` in the scikit-build source tree, *but* there are no other instances of `PythonLibs`/`PythonInterp`. I am...

> If we just hard switch, this will break all downstream packages that use the variables set by FindPythonLibs/FindPythonInterp > Yep! I totally agree ... when I started needing to...

Yeah, it seems that: ```cmake add_library(${module} MODULE ${module}) python_extension_module(${module}) ``` Has the same result as: ```cmake Python_add_library(${module} MODULE WITH_SOABI ${module}) ``` However, `python_standalone_executable` does add some target properties that I'd...