Use SMT formula satisfiability check caches

[Saloed]

Try to apply ksmt-based satisfiability check results cache

https://github.com/plan-research/cache-a-lot

https://arxiv.org/pdf/2504.07642