4 ms·
F* also uses SAT/SMT, specifically Z3.
by gsbcbdjfncnjd 2y ago
F* also uses SAT/SMT, specifically Z3.
- nextos 2y agoSure, 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.