HomeIsabelle/Phabricator
Include veriT component for "smt" method

HOL

  • An updated version of the veriT solver is now included as Isabelle component. It can be used in the smt proof method via smt (verit) or via declare [[smt_solver = verit]] in the context; see also session HOL-Word-SMT_Examples.

This refers to Isabelle/e4d707eb7d1b.

Written by makarius on Oct 19 2020, 4:59 PM.
User
Projects
None
Subscribers
None

Event Timeline