Add --dump-smt-formula argument

Author: Enrico Steffinlongo

src/goto-checker/solver_factory.cpp

@@ -149,7 +149,14 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
     options.get_option("incremental-smt2-solver");
   if(!incremental_smt2_solver.empty())
   {
-    const auto out_filename = options.get_option("outfile");
+    if(options.get_option("outfile") != "")
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "Argument --outfile is incompatible with --incremental-smt2-solver. "
+        "Use --dump-smt-formula instead.",
+        "--outfile");
+    }
+    const auto out_filename = options.get_option("dump-smt-formula");
     return get_incremental_smt2(incremental_smt2_solver, out_filename);
   }
   if(options.get_bool_option("smt2"))
@@ -332,7 +339,8 @@ solver_factoryt::get_string_refinement()
     std::move(decision_procedure), std::move(prop));
 }
 
-std::unique_ptr<std::ofstream> open_outfile_and_check(const std::string &filename)
+std::unique_ptr<std::ofstream>
+open_outfile_and_check(const std::string &filename, const std::string &arg_name)
 {
   if(filename.empty())
     return nullptr;
@@ -346,7 +354,7 @@ std::unique_ptr<std::ofstream> open_outfile_and_check(const std::string &filenam
   if(!*out)
   {
     throw invalid_command_line_argument_exceptiont(
-      "failed to open file: " + filename, "--filename");
+      "failed to open file: " + filename, arg_name);
   }
 
   std::cout << "Outputting SMTLib formula to file: " << filename << "\n";
@@ -360,7 +368,9 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_incremental_smt2(
   no_beautification();
 
   auto solver_process = util_make_unique<smt_piped_solver_processt>(
-    std::move(solver_command), message_handler, open_outfile_and_check(outfile));
+    std::move(solver_command),
+    message_handler,
+    open_outfile_and_check(outfile, "--dump-smt-formula"));
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
@@ -416,7 +426,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
   }
   else
   {
-    auto out = open_outfile_and_check(filename);
+    auto out = open_outfile_and_check(filename, "--outfile");
 
     auto smt2_conv = util_make_unique<smt2_convt>(
       ns,
@@ -558,6 +568,10 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options)
   if(cmdline.isset("outfile"))
     options.set_option("outfile", cmdline.get_value("outfile"));
 
+  if(cmdline.isset("dump-smt-formula"))
+    options.set_option(
+      "dump-smt-formula", cmdline.get_value("dump-smt-formula"));
+
   if(cmdline.isset("write-solver-stats-to"))
   {
     options.set_option(

src/goto-checker/solver_factory.h

@@ -115,6 +115,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "(refine-arrays)"                                                            \
   "(refine-arithmetic)"                                                        \
   "(outfile):"                                                                 \
+  "(dump-smt-formula):"                                                        \
   "(write-solver-stats-to):"
 
 #define HELP_SOLVER                                                            \
@@ -142,6 +143,8 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "                              command to invoke external SMT solver for\n"  \
   "                              incremental solving (experimental)\n"         \
   " --outfile filename           output formula to given file\n"               \
+  " --dump-smt-formula filename  output smt incremental formula to the\n"      \
+  "                              given file\n"                                 \
   " --write-solver-stats-to json-file\n"                                       \
   "                              collect the solver query complexity\n"