write vccs and its smt formulas in file

src/esbmc/bmc.cpp

@@ -165,14 +165,6 @@ void bmct::generate_smt_from_equation(
     "Encoding to solver time: {}s", time2string(encode_stop - encode_start));
 }
 
-// std::string bmct::generate_slhv_smt_from_equation(z3_slhv_convt& slhv_converter, symex_target_equationt &eq) {
-//   log_status("generate slhv formula from equation");
-//   std::string result;
-//   eq.convert2slhv(slhv_converter);
-//   log_status("here");
-//   return result;
-// }
-
 smt_convt::resultt
 bmct::run_decision_procedure(smt_convt &smt_conv, symex_target_equationt &eq)
 {
@@ -655,6 +647,7 @@ smt_convt::resultt bmct::run_thread(std::shared_ptr<symex_target_equationt> &eq)
     {
       runtime_solver =
         std::unique_ptr<smt_convt>(create_solver("", ns, options));
+      show_vcc(*eq);
       // log_status("smt_convt created");
       // if (options.get_bool_option("z3-slhv")) {
       //   show_vcc(*eq);

src/goto-symex/symex_target_equation.cpp

@@ -144,10 +144,6 @@ void symex_target_equationt::convert(smt_convt &smt_conv)
   if (!assertions.empty())
     smt_conv.assert_ast(smt_conv.make_n_ary_or(assertions));
   log_status("final convert result =============  ");
-
-  smt_conv.dump_smt();
-  log_status("==================================  ");
-
 }
 
 // void symex_target_equationt::convert2slhv(z3_slhv_convt& slhv_convt) {

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -54,7 +54,19 @@ z3_slhv_convt::~z3_slhv_convt() { delete_all_asts(); }
 
 smt_convt::resultt z3_slhv_convt::dec_solve() {
   log_status("z3-slhv debug: before slhv check");
+
+  const std::string &path = options.get_option("output");
+  if (path != "-")
+  {
+    std::ofstream out(path, std::ios_base::app);
+    out << "SMT formulas for VCCs:\n";
+    for(z3::expr expr : solver.assertions()) {
+      out << expr.to_string() << '\n';
+    }
+  }
+
   z3::check_result result = solver.check();
+
   log_status("z3-slhv debug: after check");
 
   if (result == z3::sat)