Do not pass around prop_conv

It's a class member anyway.

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -293,11 +293,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
   }
 }
 
-safety_checkert::resultt bmct::all_properties(
-  const goto_functionst &goto_functions,
-  prop_convt &solver)
+safety_checkert::resultt
+bmct::all_properties(const goto_functionst &goto_functions)
 {
-  bmc_all_propertiest bmc_all_properties(goto_functions, solver, *this);
+  bmc_all_propertiest bmc_all_properties(goto_functions, prop_conv, *this);
   bmc_all_properties.set_message_handler(get_message_handler());
   return bmc_all_properties();
 }

src/cbmc/bmc.cpp

@@ -126,8 +126,7 @@ void bmct::do_conversion()
   freeze_program_variables();
 }
 
-decision_proceduret::resultt
-bmct::run_decision_procedure(prop_convt &prop_conv)
+decision_proceduret::resultt bmct::run_decision_procedure()
 {
   status() << "Passing problem to "
            << prop_conv.decision_procedure_text() << eom;
@@ -345,7 +344,7 @@ safety_checkert::resultt bmct::execute(
     }
 
     if(!options.is_set("paths") || symex.path_segment_vccs > 0)
-      return decide(goto_functions, prop_conv);
+      return decide(goto_functions);
 
     return safety_checkert::resultt::PAUSED;
   }
@@ -428,16 +427,14 @@ safety_checkert::resultt bmct::run(
   return execute(goto_model);
 }
 
-safety_checkert::resultt bmct::decide(
-  const goto_functionst &goto_functions,
-  prop_convt &prop_conv)
+safety_checkert::resultt bmct::decide(const goto_functionst &goto_functions)
 {
   prop_conv.set_message_handler(get_message_handler());
 
   if(options.get_bool_option("stop-on-fail"))
-    return stop_on_fail(prop_conv);
+    return stop_on_fail();
   else
-    return all_properties(goto_functions, prop_conv);
+    return all_properties(goto_functions);
 }
 
 void bmct::show()
@@ -453,9 +450,9 @@ void bmct::show()
   }
 }
 
-safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
+safety_checkert::resultt bmct::stop_on_fail()
 {
-  switch(run_decision_procedure(prop_conv))
+  switch(run_decision_procedure())
   {
   case decision_proceduret::resultt::D_UNSATISFIABLE:
     report_success();

src/cbmc/bmc.h

@@ -177,12 +177,9 @@ class bmct:public safety_checkert
   // use gui format
   ui_message_handlert &ui_message_handler;
 
-  virtual decision_proceduret::resultt
-    run_decision_procedure(prop_convt &prop_conv);
+  virtual decision_proceduret::resultt run_decision_procedure();
 
-  virtual resultt decide(
-    const goto_functionst &,
-    prop_convt &);
+  virtual resultt decide(const goto_functionst &);
 
   void do_conversion();
 
@@ -193,10 +190,8 @@ class bmct:public safety_checkert
     return trace_optionst(options);
   }
 
-  virtual resultt all_properties(
-    const goto_functionst &goto_functions,
-    prop_convt &solver);
-  virtual resultt stop_on_fail(prop_convt &solver);
+  virtual resultt all_properties(const goto_functionst &goto_functions);
+  virtual resultt stop_on_fail();
   virtual void report_success();
   virtual void report_failure();