Trevor Hansen

I think this is fixed now. Please reopen if I've misunderstood.

Thanks for reporting the problem. I've had a go at fixing it in: 95868756ae2e2487b0f9405d17281b4d5394a476 82d76c804f0f3ba2396bdb145f9326aca5517379 Let me know if it doesn't do what you need or could be better.

> Unsure why clang passed and gcc failed. I expected both to fail. gcc-built version getting errors like this: > > ``` > /home/runner/work/stp/stp/build/tests/unit-tests/MergeSame_TestTests: error while loading shared libraries: libcadiback.so:...

You're right that STP doesn't keep learned clauses between invocations to the SAT solver. It has some simple analysis, for example if a problem is unsatisfiable, and you push more...

Thanks for the files @sreeshmaheshwar. The examples are good. Looking at b64.txt, it's got 1000 (check-sat) calls, for me default STP takes 16 seconds, STP with simplifications disabled takes about...