Smt fails to solve trivial logic goals under specific conditions

[oskgo]

MRE:

lemma addbK : right_loop idfun (^) by case. (* succeeds, demonstrating triviality *)

lemma addbK' : right_loop idfun (^) by smt(). (* times out *)

Separates out the issue with Logic from #1025

config

[main]
default_editor = "open %f"
magic = 14
memlimit = 1000
running_provers_max = 2
timelimit = 5.000000

[partial_prover]
name = "Alt-Ergo"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/alt-ergo"
version = "2.4.3"

[partial_prover]
name = "CVC4"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/cvc4"
version = "1.8"

[partial_prover]
name = "CVC5"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/cvc5"
version = "1.0.9"

[partial_prover]
name = "Z3"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/z3"
version = "4.12.6"