Warn when --outfile produces an empty formula

When all properties are simplified to true before solving, the formula
file written via --outfile contains only the solver header and no
assertions. This can be confusing to users. Add a warning message
explaining why the file is nearly empty.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

regression/cbmc/empty-formula-warning/main.c

@@ -0,0 +1,7 @@
+#include <assert.h>
+int main()
+{
+  int x = 5;
+  assert(x == 5);
+  return 0;
+}

regression/cbmc/empty-formula-warning/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--smt2 --outfile formula.smt2
+^EXIT=0$
+^SIGNAL=0$
+will not contain any assertions
+--

src/goto-checker/bmc_util.cpp

@@ -211,6 +211,16 @@ void slice(
   msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
                    << symex.get_remaining_vccs()
                    << " remaining after simplification" << messaget::eom;
+
+  if(
+    symex.get_total_vccs() > 0 && symex.get_remaining_vccs() == 0 &&
+    !options.get_option("outfile").empty())
+  {
+    const std::string outfile = options.get_option("outfile");
+    msg.warning() << "All properties were simplified to true before solving. "
+                  << "The formula written to " << outfile
+                  << " will not contain any assertions." << messaget::eom;
+  }
 }
 
 void update_properties_status_from_symex_target_equation(