4043 filter smt lemmas use only opaque use equations symmetrically#4054

Open

jberthold wants to merge 7 commits intomasterfrom 4043-filter-smt-lemmas-use-only-opaque-use-equations-symmetrically

+114-26

Commits on Sep 11, 2024

Filter SMT lemmas by what functions they relate to, for predicate checks and get-model
jberthold
committed

Commits on Sep 17, 2024

Merge branch 'master' into 4043-filter-smt-lemmas-for-predicate-checks
PetarMax
authored

Commits on Sep 25, 2024

Merge branch 'master' into 4043-filter-smt-lemmas-for-predicate-checks
PetarMax
authored

Commits on Oct 1, 2024

Merge branch 'master' into 4043-filter-smt-lemmas-for-predicate-checks
PetarMax
authored

Commits on Oct 2, 2024

Use only SMT lemmas with opaque symbols (should have none without)
jberthold
committed

Commits on Oct 3, 2024

Use both sides of equations equally when building the lemma lookup map
jberthold
committed
Format with fourmolu
github-actions
committed