From 97d19e22b5ffe6732d754360460b696bc422d26b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 1 Apr 2026 17:41:12 +0000 Subject: [PATCH] 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 --- regression/cbmc/empty-formula-warning/main.c | 7 +++++++ regression/cbmc/empty-formula-warning/test.desc | 7 +++++++ src/goto-checker/bmc_util.cpp | 10 ++++++++++ 3 files changed, 24 insertions(+) create mode 100644 regression/cbmc/empty-formula-warning/main.c create mode 100644 regression/cbmc/empty-formula-warning/test.desc diff --git a/regression/cbmc/empty-formula-warning/main.c b/regression/cbmc/empty-formula-warning/main.c new file mode 100644 index 00000000000..0d7dde8eddb --- /dev/null +++ b/regression/cbmc/empty-formula-warning/main.c @@ -0,0 +1,7 @@ +#include +int main() +{ + int x = 5; + assert(x == 5); + return 0; +} diff --git a/regression/cbmc/empty-formula-warning/test.desc b/regression/cbmc/empty-formula-warning/test.desc new file mode 100644 index 00000000000..e5ef4f5c460 --- /dev/null +++ b/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 +-- diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 5bb3d9ce459..5a818eb28f0 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/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(