Warn when --outfile produces an empty formula

doc/man/cbmc.1

@@ -547,6 +547,10 @@ The SMT solver should support the QF_AUFBV logic.
 .TP
 \fB\-\-outfile\fR filename
 output formula to given file
+.br
+If all properties are simplified to true before solving, the formula
+written to \fIfilename\fR will contain only the solver header and no
+assertions, and a status message is emitted to that effect.
 .TP
 \fB\-\-dump\-smt\-formula\fR filename
 output smt incremental formula to the given file

doc/man/jbmc.1

@@ -451,6 +451,10 @@ incremental solving (experimental)
 .TP
 \fB\-\-outfile\fR filename
 output formula to given file
+.br
+If all properties are simplified to true before solving, the formula
+written to \fIfilename\fR will contain only the solver header and no
+assertions, and a status message is emitted to that effect.
 .TP
 \fB\-\-dump\-smt\-formula\fR filename
 output smt incremental formula to the given file

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

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

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

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

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

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

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

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

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 no-new-smt paths-lifo-expected-failure
+main.c
+--smt2 --outfile formula.smt2
+^EXIT=0$
+^SIGNAL=0$
+will not contain any assertions
+--

src/cbmc/cbmc_parse_options.cpp

@@ -675,12 +675,31 @@ int cbmc_parse_optionst::doit()
       stop_on_fail_verifiert<single_path_symex_checkert> verifier(
         options, ui_message_handler, goto_model);
       (void)verifier();
+      // Note: we do not emit the "empty formula" usability warning here.
+      // Under --paths the equation is rebuilt per path and the outfile is
+      // overwritten on each non-empty path, so a per-path notion of "the
+      // formula is empty" does not correspond to anything the user can
+      // observe in the final file.
     }
     else
     {
       stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
         options, ui_message_handler, goto_model);
       (void)verifier();
+
+      // If symex generated VCCs but simplification reduced them all to true,
+      // the formula written via --outfile contains only the solver header
+      // and no assertions. Tell the user why the file is nearly empty.
+      const std::string outfile = options.get_option("outfile");
+      if(
+        !outfile.empty() && verifier.get_checker().get_total_vccs() > 0 &&
+        verifier.get_checker().get_remaining_vccs() == 0)
+      {
+        log.status() << "All properties were simplified to true before "
+                        "solving. The formula written to "
+                     << outfile << " will not contain any assertions."
+                     << messaget::eom;
+      }
     }
 
     return CPROVER_EXIT_SUCCESS;

src/goto-checker/multi_path_symex_only_checker.h

@@ -29,6 +29,22 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert
 
   resultt operator()(propertiest &) override;
 
+  /// Returns the total number of VCCs generated by symex, before
+  /// simplification.
+  std::size_t get_total_vccs() const
+  {
+    return symex.get_total_vccs();
+  }
+
+  /// Returns the number of VCCs remaining after simplification (i.e. those
+  /// still to be discharged by a solver). When this is zero but
+  /// \ref get_total_vccs returns a positive value, all properties were
+  /// simplified to true and there is nothing for the solver to do.
+  std::size_t get_remaining_vccs() const
+  {
+    return symex.get_remaining_vccs();
+  }
+
 protected:
   abstract_goto_modelt &goto_model;
   symbol_tablet symex_symbol_table;

src/goto-checker/stop_on_fail_verifier.h

@@ -74,6 +74,14 @@ class stop_on_fail_verifiert : public goto_verifiert
     incremental_goto_checker.report();
   }
 
+  /// Returns the underlying incremental goto checker. Useful for callers that
+  /// need to query checker-specific state after verification, e.g. VCC counts
+  /// when deciding whether to emit a usability warning.
+  const incremental_goto_checkerT &get_checker() const
+  {
+    return incremental_goto_checker;
+  }
+
 protected:
   abstract_goto_modelt &goto_model;
   incremental_goto_checkerT incremental_goto_checker;