SMT Solver should not bypass the termination check

[yangky11]

Here the SMT solver called by euclid_finish is bypassing the termination check. @loganrjmurphy Any idea on how this can be fixed? I'm thinking about either preventing euclid_apply from using the theorem itself or preventing SMT solvers from using local lemmas with universally quantified variables.

[FrederickPu]

I have a branch where I ported to use the smt tactic directly with the euclid axioms. Which involves generating a proof certificate so this issue no longer occurs https://github.com/project-numina/LeanEuclid/tree/to415