Module `Terms.Smt`

Translation of the constraints to an SMT problem, and resolution.

module MakeFirstOrder
  (T : Sig.TERMS)
  (S : Smtbackend.Smtlib_sig.UNTYPED_S) : 
  sig ... end

module MakeHorn
  (T : Sig.TERMS)
  (S : Smtbackend.Smtlib_sig.UNTYPED_MUZ) : 
  sig ... end

Module Terms.Smt