epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Enable reading smt-lib files with dependent types for future text interface from Stainless #182

Open vkuncak opened 2 years ago

vkuncak commented 2 years ago

We would like to make it possible to have VCs from Stainless be passed as SMT-LIB files.

This will then make interchange with other tools easier.