Merge pull request diffblue#4529 from diffblue/functions_lowering_prop_convt

functions lowering does not need prop_convt

Author: tautschnig

src/solvers/lowering/functions.cpp

@@ -62,7 +62,7 @@ void functionst::add_function_constraints(const function_infot &info)
 
       implies_exprt implication(arguments_equal_expr, equal_exprt(*it1, *it2));
 
-      prop_conv.set_to_true(implication);
+      decision_procedure.set_to_true(implication);
     }
   }
 }

src/solvers/lowering/functions.h

@@ -17,12 +17,13 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/mathematical_expr.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/prop/decision_procedure.h>
 
 class functionst
 {
 public:
-  explicit functionst(prop_convt &_prop_conv) : prop_conv(_prop_conv)
+  explicit functionst(decision_proceduret &_decision_procedure)
+    : decision_procedure(_decision_procedure)
   {
   }
 
@@ -38,7 +39,7 @@ class functionst
   }
 
 protected:
-  prop_convt &prop_conv;
+  decision_proceduret &decision_procedure;
 
   typedef std::set<function_application_exprt> applicationst;