lean-smt breaking on proof reconstruction

Stream: general

[Frederick Pu]

When lean-smt throws and unsolved goals error but does not say that it failed to prove the goal. So it seems like the reconstruction is failing. Here is what show_term esmt gives:

refine
    ?_
      (let_fun this := two_points_determine_line;
      this)

Here is the proof that I'm running:

theorem proposition_5 : ∀ (a b c d e : Point) (AB BC AC : Line),
  formTriangle a b c AB BC AC ∧ (|(a─b)| = |(a─c)|) ∧
  (between a b d) ∧ (between a c e) →
  (∠ a:b:c = ∠ a:c:b) ∧ (∠ c:b:d = ∠ b:c:e) :=
by
  euclid_intros
  euclid_apply (point_between_points_shorter_than AB b d (c─e)) as f
  euclid_apply (proposition_3 a e f a AC AB) as g
  euclid_apply (line_from_points c f) as FC
  euclid_apply (line_from_points b g) as GB
  euclid_apply (proposition_4 a f c a g b AB FC AC AC GB AB)
  euclid_apply (proposition_4 f b c g c b AB BC FC AC BC GB)
  have := (sum_angles_onlyif b a g c AB GB) (by show_term esmt)
  euclid_apply (sum_angles_onlyif c a f b AC FC)
  euclid_finish

I'm doing this on a fork of the LeanEuclid repo https://github.com/project-numina/LeanEuclid/tree/to415

[Frederick Pu]

for reference esmt is just a wrapper for smt that includes all axioms tagged with euclid. The implementation can be found here https://github.com/project-numina/LeanEuclid/blob/to415/SystemE/Tactic/ESmt.lean