projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b509f27) | patch
Connect the LFSC printer (#7323)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 11 Oct 2021 14:28:51 +0000 (09:28 -0500)
committerGitHub <noreply@github.com>
Mon, 11 Oct 2021 14:28:51 +0000 (09:28 -0500)
commit9c9c909d8815c8026b6aaa1da259672aa96d193e
tree3add0f71a6f85d3a98ddf70e6dfa9b4b60395206tree
parentb509f2700e31b4189ac76e4d0eabdde050535c0acommit | diff
Connect the LFSC printer (#7323)

This adds the option --proof-format=lfsc.

It adds an initial regression to test the LFSC printer. This will be followed up with a more comprehensive plan for regression tests.
src/options/proof_options.toml diff | blob | history
src/smt/proof_manager.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/lfsc-test-1.smt2 [new file with mode: 0644] blob