summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2014-05-15 12:51:35 -0500
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2014-05-15 12:51:35 -0500
commit839b8f788f1d240380ca72c6d245c62e8e47501b (patch)
treed26835fab14c4ae0f4c32267dad0a7a2cd27a261 /src/smt
parent478b935ba5e2b9eda4eb21f7651747c5325229b1 (diff)
Minor fixes. Add SMTCOMP 2014 script.
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c6b76e850..8ef1d1543 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3803,13 +3803,13 @@ Proof* SmtEngine::getProof() throw(ModalException) {
void SmtEngine::printInstantiations( std::ostream& out ) {
SmtScope smts(this);
if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
- out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl;
+ out << "% SZS output start Proof for " << d_filename.c_str() << std::endl;
}
if( d_theoryEngine ){
d_theoryEngine->printInstantiations( out );
}
if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
- out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl;
+ out << "% SZS output end Proof for " << d_filename.c_str() << std::endl;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback