add print smt, using --output

benchmark/case_0.c

@@ -3,9 +3,9 @@
 int main(){
     // int whatever;
     int * data = malloc(2*sizeof(int));
-    int * data2 = malloc(sizeof(int));  
-    int i = *(data + 1);
-    free(data);
+    // int * data2 = malloc(sizeof(int));  
+    // int i = *(data + 1);
+    // free(data);
     // int* j = NULL;
     // int* i = j;
     // // *(data + 1) = whatever;

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -354,6 +354,38 @@ z3_slhv_convt::convert_slhv_opts(
   }
 }
 
+
+void z3_slhv_convt::dump_smt() {
+  const std::string &path = options.get_option("output");
+  if(path == "-") {
+    print_smt_formulae(std::cout);
+  } else {
+    std::ofstream out(path);
+    print_smt_formulae(out);
+  }
+}
+
+void z3_slhv_convt::print_smt_formulae(std::ostream& dest) {
+  auto smt_formula = solver.to_smt2();
+  std::replace(smt_formula.begin(), smt_formula.end(), '\\', '_');
+  Z3_ast_vector __z3_assertions = Z3_solver_get_assertions(z3_ctx, solver);
+  // Add whatever logic is needed.
+  // Add solver specific declarations as well.
+  dest << "(set-logic SLHV)" << std::endl;
+  dest << "(set-info :smt-lib-version 2.6)\n";
+  dest << "(set-option :produce-models true)\n";
+  dest << "(declare-fun emp () IntHeap)" << std::endl;
+  dest << "(declare-fun nil () IntLoc)" << std::endl;
+  dest << "; Asserts from ESMBC starts\n";
+  dest << smt_formula; // All VCC conditions in SMTLIB format.
+  dest << "; Asserts from ESMBC ends\n";
+  dest << "(get-model)\n";
+  dest << "(exit)\n";
+  log_status(
+    "Total number of safety properties: {}",
+    Z3_ast_vector_size(z3_ctx, __z3_assertions));
+}
+
 // smt_astt z3_slhv_convt::convert_ast_slhv(const expr2tc &expr) {
 //   log_status("== convert ast slhv");
 //   expr->dump();
@@ -888,7 +920,3 @@ z3_slhv_convt::convert_slhv_opts(
 // void z3_slhv_convt::print_smt_formulae(std::ostream &dest) {
 //   log_status("TODO: slhv print smt");
 // }
-
-// void z3_slhv_convt::dump_smt() {
-//   log_status("TODO: slhv dump smt");
-// }

src/solvers/z3-slhv/z3_slhv_conv.h

@@ -59,7 +59,10 @@ class z3_slhv_convt : public z3_convt {
     smt_astt
     convert_slhv_opts(const expr2tc &expr, const std::vector<smt_astt>& args) override;
 
+    void dump_smt() override;
+
 private:
+    void print_smt_formulae(std::ostream& dest);
     std::vector<smt_astt> assertions;
 };