top | item 42511283

(no title)

gsbcbdjfncnjd | 1 year ago

F* also uses SAT/SMT, specifically Z3.

discuss

order

nextos|1 year ago

Sure, what I meant is that Dafny outsources everything to SAT/SMT. If it doesn't manage to prove things for you, it gets a bit frustrating as there is not much support for manual tactics compared to F*, Coq or Isabelle, which can also leverage SAT/SMT, but have other options.