From 29e7ba5ce9b8686832b2c0a7fcdeca7443347c50 Mon Sep 17 00:00:00 2001
From: Rod Chapman <rodchap@amazon.com>
Date: Fri, 13 Jun 2025 15:29:44 +0100
Subject: [PATCH] Change the   "No assigns clause provided ..." and   "No
 decreases clause provided..." warnings to "debug" instead of "warning" level.

These will no longer be reported at default verbosity level (6),
but can be re-instated by setting verbosity to level 10.

Signed-off-by: Rod Chapman <rodchap@amazon.com>
---
 .../dynamic-frames/dfcc_cfg_info.cpp          | 24 +++++++++----------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
index 3330c6f2617..dc8cffb044b 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
@@ -360,31 +360,31 @@ static struct contract_clausest default_loop_contract_clauses(
     else
     {
       // infer assigns clause targets if none given
-      log.warning() << "No assigns clause provided for loop " << function_id
-                    << "." << loop.latch->loop_number << " at "
-                    << loop.head->source_location() << ". The inferred set {";
+      log.debug() << "No assigns clause provided for loop " << function_id
+                  << "." << loop.latch->loop_number << " at "
+                  << loop.head->source_location() << ". The inferred set {";
       bool first = true;
       for(const auto &expr : inferred_assigns)
       {
         if(!first)
         {
-          log.warning() << ", ";
+          log.debug() << ", ";
         }
         first = false;
-        log.warning() << format(expr);
+        log.debug() << format(expr);
       }
-      log.warning() << "} might be incomplete or imprecise, please provide an "
-                       "assigns clause if the analysis fails."
-                    << messaget::eom;
+      log.debug() << "} might be incomplete or imprecise, please provide an "
+                     "assigns clause if the analysis fails."
+                  << messaget::eom;
       result.assigns = inferred_assigns;
     }
 
     if(result.decreases_clauses.empty())
     {
-      log.warning() << "No decrease clause provided for loop " << function_id
-                    << "." << loop.latch->loop_number << " at "
-                    << loop.head->source_location()
-                    << ". Termination will not be checked." << messaget::eom;
+      log.debug() << "No decrease clause provided for loop " << function_id
+                  << "." << loop.latch->loop_number << " at "
+                  << loop.head->source_location()
+                  << ". Termination will not be checked." << messaget::eom;
     }
   }
   return result;