diff --git a/src/solvers/lowering/functions.cpp b/src/solvers/lowering/functions.cpp
index 8b2f160cf16..097715a1011 100644
--- a/src/solvers/lowering/functions.cpp
+++ b/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);
     }
   }
 }
diff --git a/src/solvers/lowering/functions.h b/src/solvers/lowering/functions.h
index 89fb760ea94..36681b9c9c7 100644
--- a/src/solvers/lowering/functions.h
+++ b/src/solvers/lowering/functions.h
@@ -17,12 +17,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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;