Error when proving two theorems with smt in the same file

[tomaz1502]

If we try to build the following script:

import Smt

set_option trace.smt.debug.reconstruct true

theorem t0 (p q : Prop) : p ∧ q → q ∧ p := by
  smt

theorem t1 (p q : Prop) : p → q → p := by
  smt

The first theorem type checks, but the second one throws an error, even though our tactic is enough to prove it. This is because the second call of smt tries to define again the theorem th0, as this name is hard coded into the tactic. In order to fix we could just change the name of the theorem generated for a fresh name, with mkFreshId

[abdoo8080]

This is issue is now fixed with the change to cvc5's FFI interface.