Dynamic prelude

I've had an idea:

💥 The prelude should not be fixed. It should be reset dynamically, removing all uninterpreted function symbols (and associated SMT lemmas) that are not in the ground truth plus the predicates to be checked. 💥

What do we lose? Forall-quantified statements that we know are difficult for the solver to handle.
What do we gain? SATs and UNSATs instead of unknowns.

Why am I thinking of this - because I am running some new (potental engagement) tests and I am getting a real Unknown from Z3, and the constraints contain modInt because that is what the code uses. When the smt-lemma

rule chop ( I:Int ) => I modInt pow256 [concrete, smt-lemma]

is present, Z3 really returns Unknown, no matter how large I set the timeout, when it’s removed I get an instant SAT/UNSAT.

This means that that modInt in the SMT lemma is 🪄 soMehOw 🪄 interacting with the solver, it’s trying to define chop as a function and failing, but chop is not relevant to this query and there is no need for it to be there.

Start by tracing how the SMT prelude and smt-lemmas are assembled, focusing on the dynamic-prelude proposal and the rule chop example involving modInt and pow256. Reproduce the reported Z3 Unknown versus SAT/UNSAT behavior, then define and test when uninterpreted functions and associated lemmas should be retained.