diff options
| author | lianah <lianahady@gmail.com> | 2013-10-08 19:22:19 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-10-08 19:22:19 -0400 |
| commit | 000f574406c29df4c60947169ef527ee5316beb7 (patch) | |
| tree | e2bc0426627689ccd59d63976c9497cb9f0dc335 /src/proof/proof_manager.cpp | |
| parent | 3361081acd11178d0eb580ce91279a2ecaa7aa65 (diff) | |
added currying for uf proofs; still needs debugging
Diffstat (limited to 'src/proof/proof_manager.cpp')
| -rw-r--r-- | src/proof/proof_manager.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e1f85b93f..0c3c597da 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -131,6 +131,7 @@ void LFSCProof::toStream(std::ostream& out) { std::ostringstream paren; out << "(check \n"; d_theoryProof->printDeclarations(out, paren); + d_theoryProof->printAssertions(out, paren); out << "(: (holds cln) \n"; d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); |