More Third-Party Tools
==============================


=========================
SyGuS
=========================


SyGuS solvers for invariant synthesis/generation:

* **CVC5** (`github repository <https://github.com/cvc5/cvc5>`_)
  
  An open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

* **LoopInvGen** (`github repository <https://github.com/SaswatPadhi/LoopInvGen>`_)
  
  A data-driven tool that generates provably sufficient loop invariants for program verification.

* **DryadSynth** (`github repository <https://github.com/rainoftime/DryadSynth>`_)
  
  A SyGuS solver that reconciles enumerative and deductive program synthesis.

Non-linear Invariant
-------------------

* **PolyHorn** (`github repository <https://github.com/milad-saadat/PolyHorn>`_)

  Supports CHC frontend for non-linear invariant generation.