Remove debug code from SMT

polgreen · Apr 30, 2021 · c629eb2 · c629eb2
1 parent 7948824
commit c629eb2
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git 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
@@ -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<std::string> &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))<<messaget::eom;
+    // log.debug() << "Response matches " << expr2sygus(get(application.handle))<<messaget::eom;
     return CONSISTENT; // done, SAT
   }
   {
 
     function_application_exprt func_app(application_expr.function(), inputs);
 
-    log.debug() << "Response does not match " << expr2sygus(get(application.handle)) << messaget::eom;
+    // log.debug() << "Response does not match " << expr2sygus(get(application.handle)) << messaget::eom;
 
     // add a constraint that enforces this equality
     auto response_equality = equal_exprt(application.handle, response);