From c629eb28d165631cd364fd6329560e33731c31a8 Mon Sep 17 00:00:00 2001 From: Elizabeth Polgreen Date: Fri, 30 Apr 2021 11:35:11 +0100 Subject: [PATCH] Remove debug code from SMT --- src/delphi/verification/oracle_interface.cpp | 6 +++--- src/delphi/verification/oracle_solver.cpp | 14 +++++++------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/delphi/verification/oracle_interface.cpp b/src/delphi/verification/oracle_interface.cpp index 74b0e03..080d42f 100644 --- a/src/delphi/verification/oracle_interface.cpp +++ b/src/delphi/verification/oracle_interface.cpp @@ -205,10 +205,10 @@ void oracle_interfacet::get_oracle_constraints( argv.push_back(stream.str()); } - log.status() << "Running oracle (synthesis)"; + log.debug() << "Running oracle (synthesis)"; for (auto &arg : argv) - log.status() << ' ' << arg; - log.status() << messaget::eom; + log.debug() << ' ' << arg; + log.debug() << messaget::eom; // run the oracle binary std::ostringstream stdout_stream; diff --git a/src/delphi/verification/oracle_solver.cpp b/src/delphi/verification/oracle_solver.cpp index a8e6c05..89af14e 100644 --- a/src/delphi/verification/oracle_solver.cpp +++ b/src/delphi/verification/oracle_solver.cpp @@ -129,10 +129,10 @@ oracle_solvert::check_resultt oracle_solvert::check_oracles() exprt oracle_solvert::make_oracle_call(const std::string &binary_name, const std::vector &argv) { - log.status() << "Running oracle (verification) "; - for (auto &arg : argv) - log.status() << ' ' << arg; - log.status() << messaget::eom; + // log.debug() << "Running oracle (verification) "; + // for (auto &arg : argv) + // log.debug() << ' ' << arg; + // log.debug() << messaget::eom; // run the oracle binary std::ostringstream stdout_stream; @@ -146,7 +146,7 @@ exprt oracle_solvert::make_oracle_call(const std::string &binary_name, const std if (run_result != 0 && run_result !=10) { - log.status() << "oracle " << binary_name << " has failed" << messaget::eom; + log.error() << "oracle " << binary_name << " has failed" << messaget::eom; assert(0); return nil_exprt(); } @@ -223,14 +223,14 @@ oracle_solvert::check_resultt oracle_solvert::check_oracle( // check whether the result is consistent with the model if(response == get(application.handle)) { - log.debug() << "Response matches " << expr2sygus(get(application.handle))<