projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 879a5f6) | patch
Use string stream for proofs instead of tmp files (#2841)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 27 Feb 2019 00:49:59 +0000 (00:49 +0000)
committerGitHub <noreply@github.com>
Wed, 27 Feb 2019 00:49:59 +0000 (00:49 +0000)
commit933cd31e994148cd457cb110734aa23423777fec
tree17add3eb575d24b5a3fd0c24cbe4a5e2b0b16b26tree
parent879a5f6b5e0c259571e7dbe0d7633a19e982148dcommit | diff
Use string stream for proofs instead of tmp files (#2841)

This commit changes CVC4 to use a string stream instead of a temporary
files for proof checking. Note: This change requires a version of LFSC
that supports checking streams (see
https://github.com/CVC4/LFSC/pull/14).

Tested: `make check` passed, changing `holds` to `xholds` in the proof
produced by proof_manager.cpp makes the proofs fail.
src/smt/smt_engine_check_proof.cpp diff | blob | history