diff --git a/jbmc/src/jbmc/all_properties.cpp b/jbmc/src/jbmc/all_properties.cpp
index 6b6ec88b441..2205d333450 100644
--- a/jbmc/src/jbmc/all_properties.cpp
+++ b/jbmc/src/jbmc/all_properties.cpp
@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/json.h>
 #include <util/xml.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/prop/decision_procedure.h>
 #include <solvers/sat/satcheck.h>
 
 #include <goto-programs/json_goto_trace.h>
@@ -61,7 +61,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   auto solver_start = std::chrono::steady_clock::now();
 
   convert_symex_target_equation(
-    bmc.equation, bmc.prop_conv, get_message_handler());
+    bmc.equation, bmc.decision_procedure, get_message_handler());
   bmc.freeze_program_variables();
 
   // Collect _all_ goals in `goal_map'.
@@ -301,7 +301,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 safety_checkert::resultt
 bmct::all_properties(const goto_functionst &goto_functions)
 {
-  bmc_all_propertiest bmc_all_properties(goto_functions, prop_conv, *this);
+  bmc_all_propertiest bmc_all_properties(
+    goto_functions, decision_procedure, *this);
   bmc_all_properties.set_message_handler(get_message_handler());
   return bmc_all_properties();
 }
diff --git a/jbmc/src/jbmc/all_properties_class.h b/jbmc/src/jbmc/all_properties_class.h
index a5fc881ada4..e1b34d0e380 100644
--- a/jbmc/src/jbmc/all_properties_class.h
+++ b/jbmc/src/jbmc/all_properties_class.h
@@ -22,7 +22,7 @@ class bmc_all_propertiest : public cover_goalst::observert, public messaget
 public:
   bmc_all_propertiest(
     const goto_functionst &_goto_functions,
-    prop_convt &_solver,
+    decision_procedure_incrementalt &_solver,
     bmct &_bmc)
     : goto_functions(_goto_functions), solver(_solver), bmc(_bmc)
   {
@@ -96,7 +96,7 @@ class bmc_all_propertiest : public cover_goalst::observert, public messaget
 
 protected:
   const goto_functionst &goto_functions;
-  prop_convt &solver;
+  decision_procedure_incrementalt &solver;
   bmct &bmc;
 
   virtual void report(const cover_goalst &cover_goals);
diff --git a/jbmc/src/jbmc/bmc.cpp b/jbmc/src/jbmc/bmc.cpp
index 7cb6f68f95b..f5a29ffe3c5 100644
--- a/jbmc/src/jbmc/bmc.cpp
+++ b/jbmc/src/jbmc/bmc.cpp
@@ -42,19 +42,20 @@ void bmct::freeze_program_variables()
 
 decision_proceduret::resultt bmct::run_decision_procedure()
 {
-  status() << "Passing problem to " << prop_conv.decision_procedure_text()
-           << eom;
+  status() << "Passing problem to "
+           << decision_procedure.decision_procedure_text() << eom;
 
   auto solver_start = std::chrono::steady_clock::now();
 
-  convert_symex_target_equation(equation, prop_conv, get_message_handler());
+  convert_symex_target_equation(
+    equation, decision_procedure, get_message_handler());
 
   // hook for cegis to freeze synthesis program vars
   freeze_program_variables();
 
-  status() << "Running " << prop_conv.decision_procedure_text() << eom;
+  status() << "Running " << decision_procedure.decision_procedure_text() << eom;
 
-  decision_proceduret::resultt dec_result = prop_conv();
+  decision_proceduret::resultt dec_result = decision_procedure();
 
   {
     auto solver_stop = std::chrono::steady_clock::now();
@@ -207,11 +208,11 @@ safety_checkert::resultt bmct::stop_on_fail()
       {
         // NOLINTNEXTLINE(whitespace/braces)
         counterexample_beautificationt{ui_message_handler}(
-          dynamic_cast<boolbvt &>(prop_conv), equation);
+          dynamic_cast<boolbvt &>(decision_procedure), equation);
       }
 
       build_error_trace(
-        error_trace, ns, equation, prop_conv, ui_message_handler);
+        error_trace, ns, equation, decision_procedure, ui_message_handler);
       output_error_trace(error_trace, ns, trace_options(), ui_message_handler);
       output_graphml(error_trace, ns, options);
     }
@@ -265,12 +266,11 @@ int bmct::do_language_agnostic_bmc(
     {
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
-      prop_convt &pc = cbmc_solver->prop_conv();
       bmct bmc(
         opts,
         symbol_table,
         ui,
-        pc,
+        cbmc_solver->decision_procedure_incremental(),
         *worklist,
         callback_after_symex,
         guard_manager);
@@ -314,13 +314,12 @@ int bmct::do_language_agnostic_bmc(
     {
       std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
         solvers.get_solver();
-      prop_convt &pc = cbmc_solver->prop_conv();
       path_storaget::patht &resume = worklist->peek();
       path_explorert pe(
         opts,
         symbol_table,
         ui,
-        pc,
+        cbmc_solver->decision_procedure_incremental(),
         resume.equation,
         resume.state,
         *worklist,
diff --git a/jbmc/src/jbmc/bmc.h b/jbmc/src/jbmc/bmc.h
index 44c0754d3aa..21fa341b570 100644
--- a/jbmc/src/jbmc/bmc.h
+++ b/jbmc/src/jbmc/bmc.h
@@ -30,7 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
-#include <solvers/prop/decision_procedure.h>
+#include <solvers/prop/decision_procedure_incremental.h>
 
 class cbmc_solverst;
 
@@ -68,7 +68,7 @@ class bmct : public safety_checkert
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
     ui_message_handlert &_message_handler,
-    prop_convt &_prop_conv,
+    decision_procedure_incrementalt &_decision_procedure,
     path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex,
     guard_managert &guard_manager)
@@ -86,7 +86,7 @@ class bmct : public safety_checkert
         options,
         path_storage,
         guard_manager),
-      prop_conv(_prop_conv),
+      decision_procedure(_decision_procedure),
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
@@ -141,7 +141,7 @@ class bmct : public safety_checkert
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
     ui_message_handlert &_message_handler,
-    prop_convt &_prop_conv,
+    decision_procedure_incrementalt &_decision_procedure,
     symex_target_equationt &_equation,
     path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex,
@@ -160,7 +160,7 @@ class bmct : public safety_checkert
         options,
         path_storage,
         guard_manager),
-      prop_conv(_prop_conv),
+      decision_procedure(_decision_procedure),
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
@@ -180,7 +180,7 @@ class bmct : public safety_checkert
   guard_managert &guard_manager;
   path_storaget &path_storage;
   symex_bmct symex;
-  prop_convt &prop_conv;
+  decision_procedure_incrementalt &decision_procedure;
   std::unique_ptr<memory_model_baset> memory_model;
   // use gui format
   ui_message_handlert &ui_message_handler;
@@ -235,7 +235,7 @@ class path_explorert : public bmct
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
     ui_message_handlert &_message_handler,
-    prop_convt &_prop_conv,
+    decision_procedure_incrementalt &_decision_procedure,
     symex_target_equationt &saved_equation,
     const goto_symex_statet &saved_state,
     path_storaget &path_storage,
@@ -245,7 +245,7 @@ class path_explorert : public bmct
         _options,
         outer_symbol_table,
         _message_handler,
-        _prop_conv,
+        _decision_procedure,
         saved_equation,
         path_storage,
         callback_after_symex,
diff --git a/src/cbmc/README.md b/src/cbmc/README.md
index c734456f9a1..72995dfbd6e 100644
--- a/src/cbmc/README.md
+++ b/src/cbmc/README.md
@@ -96,7 +96,7 @@ each assertion was violated. This is constructed using `build_goto_trace`, which
 queries the backend asking what value was chosen for each program variable on
 the path from the start of the program to the relevant assertion. For more
 details on how the trace is populated see the documentation for
-`build_goto_trace` for `prop_convt::get`, the function used to query the
+`build_goto_trace` for `decision_proceduret::get`, the function used to query the
 backend.
 
 ## Path-symex
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index e39bbede197..82aa4eb4b3a 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -25,7 +25,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <linking/static_lifetime_init.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/prop/decision_procedure.h>
 
 #include <util/make_unique.h>
 #include <util/ui_message.h>
@@ -42,13 +42,13 @@ void build_error_trace(
   goto_tracet &goto_trace,
   const namespacet &ns,
   const symex_target_equationt &symex_target_equation,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   ui_message_handlert &ui_message_handler)
 {
   messaget log(ui_message_handler);
   message_building_error_trace(log);
 
-  build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace);
+  build_goto_trace(symex_target_equation, decision_procedure, ns, goto_trace);
 }
 
 ssa_step_predicatet
@@ -56,9 +56,9 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
 {
   return [property_id](
            symex_target_equationt::SSA_stepst::const_iterator step,
-           const prop_convt &prop_conv) {
+           const decision_proceduret &decision_procedure) {
     return step->is_assert() && step->get_property_id() == property_id &&
-           prop_conv.l_get(step->cond_literal).is_false();
+           decision_procedure.l_get(step->cond_literal).is_false();
   };
 }
 
@@ -105,14 +105,14 @@ void output_error_trace(
 
 void freeze_guards(
   const symex_target_equationt &equation,
-  prop_convt &prop_conv)
+  decision_procedure_incrementalt &decision_procedure)
 {
   for(const auto &step : equation.SSA_steps)
   {
     if(!step.guard_literal.is_constant())
-      prop_conv.set_frozen(step.guard_literal);
+      decision_procedure.set_frozen(step.guard_literal);
     if(step.is_assert() && !step.cond_literal.is_constant())
-      prop_conv.set_frozen(step.cond_literal);
+      decision_procedure.set_frozen(step.cond_literal);
   }
 }
 
@@ -162,14 +162,14 @@ void output_graphml(
 
 void convert_symex_target_equation(
   symex_target_equationt &equation,
-  prop_convt &prop_conv,
+  decision_proceduret &decision_procedure,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);
   msg.status() << "converting SSA" << messaget::eom;
 
   // convert SSA
-  equation.convert(prop_conv);
+  equation.convert(decision_procedure);
 }
 
 std::unique_ptr<memory_model_baset>
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 6c39c116ed0..5faf74fab80 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -28,7 +28,8 @@ class memory_model_baset;
 class message_handlert;
 class namespacet;
 class optionst;
-class prop_convt;
+class decision_proceduret;
+class decision_procedure_incrementalt;
 class symex_bmct;
 class symex_target_equationt;
 struct trace_optionst;
@@ -36,7 +37,7 @@ class ui_message_handlert;
 
 void convert_symex_target_equation(
   symex_target_equationt &,
-  prop_convt &,
+  decision_proceduret &,
   message_handlert &);
 
 /// Returns a function that checks whether an SSA step is an assertion
@@ -51,7 +52,7 @@ void build_error_trace(
   goto_tracet &,
   const namespacet &,
   const symex_target_equationt &,
-  const prop_convt &,
+  const decision_proceduret &,
   ui_message_handlert &);
 
 void output_error_trace(
@@ -60,7 +61,9 @@ void output_error_trace(
   const trace_optionst &,
   ui_message_handlert &);
 
-void freeze_guards(const symex_target_equationt &, prop_convt &);
+void freeze_guards(
+  const symex_target_equationt &,
+  decision_procedure_incrementalt &);
 
 void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
 void output_graphml(
diff --git a/src/goto-checker/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp
index 2f35b90bdea..d9696db8b4c 100644
--- a/src/goto-checker/counterexample_beautification.cpp
+++ b/src/goto-checker/counterexample_beautification.cpp
@@ -26,7 +26,7 @@ counterexample_beautificationt::counterexample_beautificationt(
 }
 
 void counterexample_beautificationt::get_minimization_list(
-  prop_convt &prop_conv,
+  decision_proceduret &decision_procedure,
   const symex_target_equationt &equation,
   minimization_listt &minimization_list)
 {
@@ -41,7 +41,7 @@ void counterexample_beautificationt::get_minimization_list(
       it->is_assignment() &&
       it->assignment_type == symex_targett::assignment_typet::STATE)
     {
-      if(!prop_conv.l_get(it->guard_literal).is_false())
+      if(!decision_procedure.l_get(it->guard_literal).is_false())
       {
         const typet &type = it->ssa_lhs.type();
 
@@ -69,7 +69,7 @@ void counterexample_beautificationt::get_minimization_list(
 
 symex_target_equationt::SSA_stepst::const_iterator
 counterexample_beautificationt::get_failed_property(
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const symex_target_equationt &equation)
 {
   // find failed property
@@ -79,8 +79,9 @@ counterexample_beautificationt::get_failed_property(
       it != equation.SSA_steps.end();
       it++)
     if(
-      it->is_assert() && prop_conv.l_get(it->guard_literal).is_true() &&
-      prop_conv.l_get(it->cond_literal).is_false())
+      it->is_assert() &&
+      decision_procedure.l_get(it->guard_literal).is_true() &&
+      decision_procedure.l_get(it->cond_literal).is_false())
       return it;
 
   UNREACHABLE;
diff --git a/src/goto-checker/counterexample_beautification.h b/src/goto-checker/counterexample_beautification.h
index e1c73ae439f..21d0db28c4c 100644
--- a/src/goto-checker/counterexample_beautification.h
+++ b/src/goto-checker/counterexample_beautification.h
@@ -28,14 +28,14 @@ class counterexample_beautificationt
 
 protected:
   void get_minimization_list(
-    prop_convt &prop_conv,
+    decision_proceduret &decision_procedure,
     const symex_target_equationt &equation,
     minimization_listt &minimization_list);
 
   void minimize(const exprt &expr, class prop_minimizet &prop_minimize);
 
   symex_target_equationt::SSA_stepst::const_iterator get_failed_property(
-    const prop_convt &prop_conv,
+    const decision_proceduret &decision_procedure,
     const symex_target_equationt &equation);
 
   // the failed property
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
index 9f59452f306..2819ca62574 100644
--- a/src/goto-checker/goto_symex_fault_localizer.cpp
+++ b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -11,13 +11,11 @@ Author: Peter Schrammel
 
 #include "goto_symex_fault_localizer.h"
 
-#include <solvers/prop/prop_conv.h>
-
 goto_symex_fault_localizert::goto_symex_fault_localizert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
   const symex_target_equationt &equation,
-  prop_convt &solver)
+  decision_procedure_incrementalt &solver)
   : options(options),
     ui_message_handler(ui_message_handler),
     equation(equation),
diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/src/goto-checker/goto_symex_fault_localizer.h
index 4d96eb2e703..a59fe0327e3 100644
--- a/src/goto-checker/goto_symex_fault_localizer.h
+++ b/src/goto-checker/goto_symex_fault_localizer.h
@@ -18,6 +18,8 @@ Author: Peter Schrammel
 
 #include <goto-symex/symex_target_equation.h>
 
+#include <solvers/prop/decision_procedure_incremental.h>
+
 #include "fault_localization_provider.h"
 
 class goto_symex_fault_localizert
@@ -27,7 +29,7 @@ class goto_symex_fault_localizert
     const optionst &options,
     ui_message_handlert &ui_message_handler,
     const symex_target_equationt &equation,
-    prop_convt &solver);
+    decision_procedure_incrementalt &solver);
 
   fault_location_infot operator()(const irep_idt &failed_property_id);
 
@@ -35,7 +37,7 @@ class goto_symex_fault_localizert
   const optionst &options;
   ui_message_handlert &ui_message_handler;
   const symex_target_equationt &equation;
-  prop_convt &solver;
+  decision_procedure_incrementalt &solver;
 
   /// A localization point is a goto instruction that is potentially at fault
   typedef std::map<literalt, fault_location_infot::score_mapt::iterator>
diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp
index c474ad14bd5..3e6ad49abff 100644
--- a/src/goto-checker/goto_symex_property_decider.cpp
+++ b/src/goto-checker/goto_symex_property_decider.cpp
@@ -23,7 +23,9 @@ goto_symex_property_decidert::goto_symex_property_decidert(
     ns,
     ui_message_handler,
     ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI);
+
   solver = solvers.get_solver();
+  decision_procedure = &solver->decision_procedure_incremental();
 }
 
 exprt goto_symex_property_decidert::goalt::as_expr() const
@@ -69,7 +71,7 @@ void goto_symex_property_decidert::convert_goals()
     // Our goal is to falsify a property, i.e., we will
     // add the negation of the property as goal.
     goal_pair.second.condition =
-      !solver->prop_conv().convert(goal_pair.second.as_expr());
+      !decision_procedure->convert(goal_pair.second.as_expr());
   }
 }
 
@@ -78,7 +80,7 @@ void goto_symex_property_decidert::freeze_goal_variables()
   for(const auto &goal_pair : goal_map)
   {
     if(!goal_pair.second.condition.is_constant())
-      solver->prop_conv().set_frozen(goal_pair.second.condition);
+      decision_procedure->set_frozen(goal_pair.second.condition);
   }
 }
 
@@ -98,17 +100,18 @@ void goto_symex_property_decidert::add_constraint_from_goals(
   }
 
   // this is 'false' if there are no disjuncts
-  solver->prop_conv().set_to_true(disjunction(disjuncts));
+  decision_procedure->set_to_true(disjunction(disjuncts));
 }
 
 decision_proceduret::resultt goto_symex_property_decidert::solve()
 {
-  return solver->prop_conv()();
+  return (*decision_procedure)();
 }
 
-prop_convt &goto_symex_property_decidert::get_solver() const
+decision_procedure_incrementalt &
+goto_symex_property_decidert::get_solver() const
 {
-  return solver->prop_conv();
+  return *decision_procedure;
 }
 
 symex_target_equationt &goto_symex_property_decidert::get_equation() const
@@ -129,7 +132,7 @@ void goto_symex_property_decidert::update_properties_status_from_goals(
     {
       auto &status = properties.at(goal_pair.first).status;
       if(
-        solver->prop_conv().l_get(goal_pair.second.condition).is_true() &&
+        decision_procedure->l_get(goal_pair.second.condition).is_true() &&
         status != property_statust::FAIL)
       {
         status |= property_statust::FAIL;
diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h
index 6ff272fdce3..2bbbd9fe1ce 100644
--- a/src/goto-checker/goto_symex_property_decider.h
+++ b/src/goto-checker/goto_symex_property_decider.h
@@ -49,7 +49,7 @@ class goto_symex_property_decidert
   decision_proceduret::resultt solve();
 
   /// Returns the solver instance
-  prop_convt &get_solver() const;
+  decision_procedure_incrementalt &get_solver() const;
 
   /// Return the equation associated with this instance
   symex_target_equationt &get_equation() const;
@@ -72,6 +72,7 @@ class goto_symex_property_decidert
   ui_message_handlert &ui_message_handler;
   symex_target_equationt &equation;
   std::unique_ptr<solver_factoryt::solvert> solver;
+  decision_procedure_incrementalt *decision_procedure = nullptr;
 
   struct goalt
   {
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index 753cf92c450..9674200e3ce 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -25,8 +25,8 @@ Author: Daniel Kroening, Peter Schrammel
 #endif
 
 #include <solvers/flattening/bv_dimacs.h>
+#include <solvers/prop/decision_procedure_incremental.h>
 #include <solvers/prop/prop.h>
-#include <solvers/prop/prop_conv.h>
 #include <solvers/prop/solver_resource_limits.h>
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/sat/dimacs_cnf.h>
@@ -45,29 +45,39 @@ solver_factoryt::solver_factoryt(
 {
 }
 
-solver_factoryt::solvert::solvert(std::unique_ptr<prop_convt> p)
-  : prop_conv_ptr(std::move(p))
+solver_factoryt::solvert::solvert(std::unique_ptr<decision_proceduret> p)
+  : decision_procedure_ptr(std::move(p))
 {
 }
 
 solver_factoryt::solvert::solvert(
-  std::unique_ptr<prop_convt> p1,
+  std::unique_ptr<decision_proceduret> p1,
   std::unique_ptr<propt> p2)
-  : prop_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
+  : prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
 {
 }
 
 solver_factoryt::solvert::solvert(
-  std::unique_ptr<prop_convt> p1,
+  std::unique_ptr<decision_proceduret> p1,
   std::unique_ptr<std::ofstream> p2)
-  : ofstream_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
+  : ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
 {
 }
 
-prop_convt &solver_factoryt::solvert::prop_conv() const
+decision_proceduret &solver_factoryt::solvert::decision_procedure() const
 {
-  PRECONDITION(prop_conv_ptr != nullptr);
-  return *prop_conv_ptr;
+  PRECONDITION(decision_procedure_ptr != nullptr);
+  return *decision_procedure_ptr;
+}
+
+decision_procedure_incrementalt &
+solver_factoryt::solvert::decision_procedure_incremental() const
+{
+  PRECONDITION(decision_procedure_ptr != nullptr);
+  decision_procedure_incrementalt *solver =
+    dynamic_cast<decision_procedure_incrementalt *>(&*decision_procedure_ptr);
+  INVARIANT(solver != nullptr, "incremental decision procedure required");
+  return *solver;
 }
 
 propt &solver_factoryt::solvert::prop() const
@@ -76,7 +86,8 @@ propt &solver_factoryt::solvert::prop() const
   return *prop_ptr;
 }
 
-void solver_factoryt::set_prop_conv_time_limit(prop_convt &prop_conv)
+void solver_factoryt::set_decision_procedure_time_limit(
+  decision_proceduret &decision_procedure)
 {
   const int timeout_seconds =
     options.get_signed_int_option("solver-time-limit");
@@ -84,12 +95,13 @@ void solver_factoryt::set_prop_conv_time_limit(prop_convt &prop_conv)
   if(timeout_seconds > 0)
   {
     solver_resource_limitst *solver =
-      dynamic_cast<solver_resource_limitst *>(&prop_conv);
+      dynamic_cast<solver_resource_limitst *>(&decision_procedure);
     if(solver == nullptr)
     {
       messaget log(message_handler);
       log.warning() << "cannot set solver time limit on "
-                    << prop_conv.decision_procedure_text() << messaget::eom;
+                    << decision_procedure.decision_procedure_text()
+                    << messaget::eom;
       return;
     }
 
@@ -97,9 +109,10 @@ void solver_factoryt::set_prop_conv_time_limit(prop_convt &prop_conv)
   }
 }
 
-void solver_factoryt::solvert::set_prop_conv(std::unique_ptr<prop_convt> p)
+void solver_factoryt::solvert::set_decision_procedure(
+  std::unique_ptr<decision_proceduret> p)
 {
-  prop_conv_ptr = std::move(p);
+  decision_procedure_ptr = std::move(p);
 }
 
 void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
@@ -179,8 +192,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
   else if(options.get_option("arrays-uf") == "always")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
 
-  set_prop_conv_time_limit(*bv_pointers);
-  solver->set_prop_conv(std::move(bv_pointers));
+  set_decision_procedure_time_limit(*bv_pointers);
+  solver->set_decision_procedure(std::move(bv_pointers));
 
   return solver;
 }
@@ -225,9 +238,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
   info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
   info.message_handler = &message_handler;
 
-  auto prop_conv = util_make_unique<bv_refinementt>(info);
-  set_prop_conv_time_limit(*prop_conv);
-  return util_make_unique<solvert>(std::move(prop_conv), std::move(prop));
+  auto decision_procedure = util_make_unique<bv_refinementt>(info);
+  set_decision_procedure_time_limit(*decision_procedure);
+  return util_make_unique<solvert>(
+    std::move(decision_procedure), std::move(prop));
 }
 
 /// the string refinement adds to the bit vector refinement specifications for
@@ -249,9 +263,10 @@ solver_factoryt::get_string_refinement()
   info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
   info.message_handler = &message_handler;
 
-  auto prop_conv = util_make_unique<string_refinementt>(info);
-  set_prop_conv_time_limit(*prop_conv);
-  return util_make_unique<solvert>(std::move(prop_conv), std::move(prop));
+  auto decision_procedure = util_make_unique<string_refinementt>(info);
+  set_decision_procedure_time_limit(*decision_procedure);
+  return util_make_unique<solvert>(
+    std::move(decision_procedure), std::move(prop));
 }
 
 std::unique_ptr<solver_factoryt::solvert>
@@ -284,7 +299,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
 
     smt2_dec->set_message_handler(message_handler);
 
-    set_prop_conv_time_limit(*smt2_dec);
+    set_decision_procedure_time_limit(*smt2_dec);
     return util_make_unique<solvert>(std::move(smt2_dec));
   }
   else if(filename == "-")
@@ -300,7 +315,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory = true;
 
-    set_prop_conv_time_limit(*smt2_conv);
+    set_decision_procedure_time_limit(*smt2_conv);
     return util_make_unique<solvert>(std::move(smt2_conv));
   }
   else
@@ -328,7 +343,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory = true;
 
-    set_prop_conv_time_limit(*smt2_conv);
+    set_decision_procedure_time_limit(*smt2_conv);
     return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
   }
 }
diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h
index b8b9c50a549..cd6954eff68 100644
--- a/src/goto-checker/solver_factory.h
+++ b/src/goto-checker/solver_factory.h
@@ -20,7 +20,7 @@ class message_handlert;
 class namespacet;
 class optionst;
 class propt;
-class prop_convt;
+class decision_proceduret;
 
 class solver_factoryt
 {
@@ -38,21 +38,24 @@ class solver_factoryt
   {
   public:
     solvert() = default;
-    explicit solvert(std::unique_ptr<prop_convt> p);
-    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2);
-    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2);
-
-    prop_convt &prop_conv() const;
+    explicit solvert(std::unique_ptr<decision_proceduret> p);
+    solvert(std::unique_ptr<decision_proceduret> p1, std::unique_ptr<propt> p2);
+    solvert(
+      std::unique_ptr<decision_proceduret> p1,
+      std::unique_ptr<std::ofstream> p2);
+
+    decision_proceduret &decision_procedure() const;
+    decision_procedure_incrementalt &decision_procedure_incremental() const;
     propt &prop() const;
 
-    void set_prop_conv(std::unique_ptr<prop_convt> p);
+    void set_decision_procedure(std::unique_ptr<decision_proceduret> p);
     void set_prop(std::unique_ptr<propt> p);
     void set_ofstream(std::unique_ptr<std::ofstream> p);
 
     // the objects are deleted in the opposite order they appear below
     std::unique_ptr<std::ofstream> ofstream_ptr;
     std::unique_ptr<propt> prop_ptr;
-    std::unique_ptr<prop_convt> prop_conv_ptr;
+    std::unique_ptr<decision_proceduret> decision_procedure_ptr;
   };
 
   /// Returns a solvert object
@@ -74,10 +77,11 @@ class solver_factoryt
 
   smt2_dect::solvert get_smt2_solver_type() const;
 
-  /// Sets the timeout of \p prop_conv if the `solver-time-limit` option
-  /// has a positive value (in seconds).
+  /// Sets the timeout of \p decision_procedure if the `solver-time-limit`
+  /// option has a positive value (in seconds).
   /// \note Most solvers silently ignore the time limit at the moment.
-  void set_prop_conv_time_limit(prop_convt &prop_conv);
+  void
+  set_decision_procedure_time_limit(decision_proceduret &decision_procedure);
 
   // consistency checks during solver creation
   void no_beautification();
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
index 7a81b6f312f..f0ea4c8437c 100644
--- a/src/goto-instrument/accelerate/scratch_program.h
+++ b/src/goto-instrument/accelerate/scratch_program.h
@@ -90,7 +90,7 @@ class scratch_programt:public goto_programt
   std::unique_ptr<propt> satcheck;
   bv_pointerst satchecker;
   smt2_dect z3;
-  prop_convt *checker;
+  decision_proceduret *checker;
   static optionst get_default_options();
 };
 
diff --git a/src/goto-symex/README.md b/src/goto-symex/README.md
index d9f63ec3a78..9511985995d 100644
--- a/src/goto-symex/README.md
+++ b/src/goto-symex/README.md
@@ -260,7 +260,7 @@ In the \ref goto-symex directory.
 
 **Key classes:**
 * \ref symex_target_equationt
-* \ref prop_convt
+* \ref decision_proceduret
 * \ref bmct
 * \ref counterexample_beautificationt
 
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index e8b68012bcd..266245aa647 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -20,13 +20,12 @@ Author: Daniel Kroening
 
 #include <goto-programs/goto_functions.h>
 
-#include <solvers/prop/prop_conv.h>
-#include <solvers/prop/prop.h>
+#include <solvers/prop/decision_procedure.h>
 
 #include "partial_order_concurrency.h"
 
 static exprt build_full_lhs_rec(
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   const exprt &src_original, // original identifiers
   const exprt &src_ssa)      // renamed identifiers
@@ -39,17 +38,18 @@ static exprt build_full_lhs_rec(
   if(id==ID_index)
   {
     // get index value from src_ssa
-    exprt index_value=prop_conv.get(to_index_expr(src_ssa).index());
+    exprt index_value = decision_procedure.get(to_index_expr(src_ssa).index());
 
     if(index_value.is_not_nil())
     {
       simplify(index_value, ns);
       index_exprt tmp=to_index_expr(src_original);
       tmp.index()=index_value;
-      tmp.array()=
-        build_full_lhs_rec(prop_conv, ns,
-          to_index_expr(src_original).array(),
-          to_index_expr(src_ssa).array());
+      tmp.array() = build_full_lhs_rec(
+        decision_procedure,
+        ns,
+        to_index_expr(src_original).array(),
+        to_index_expr(src_ssa).array());
       return std::move(tmp);
     }
 
@@ -58,8 +58,9 @@ static exprt build_full_lhs_rec(
   else if(id==ID_member)
   {
     member_exprt tmp=to_member_expr(src_original);
-    tmp.struct_op()=build_full_lhs_rec(
-      prop_conv, ns,
+    tmp.struct_op() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
       to_member_expr(src_original).struct_op(),
       to_member_expr(src_ssa).struct_op());
   }
@@ -67,13 +68,19 @@ static exprt build_full_lhs_rec(
   {
     if_exprt tmp2=to_if_expr(src_original);
 
-    tmp2.false_case()=build_full_lhs_rec(prop_conv, ns,
-      tmp2.false_case(), to_if_expr(src_ssa).false_case());
+    tmp2.false_case() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      tmp2.false_case(),
+      to_if_expr(src_ssa).false_case());
 
-    tmp2.true_case()=build_full_lhs_rec(prop_conv, ns,
-      tmp2.true_case(), to_if_expr(src_ssa).true_case());
+    tmp2.true_case() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      tmp2.true_case(),
+      to_if_expr(src_ssa).true_case());
 
-    exprt tmp=prop_conv.get(to_if_expr(src_ssa).cond());
+    exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond());
 
     if(tmp.is_true())
       return tmp2.true_case();
@@ -85,8 +92,11 @@ static exprt build_full_lhs_rec(
   else if(id==ID_typecast)
   {
     typecast_exprt tmp=to_typecast_expr(src_original);
-    tmp.op()=build_full_lhs_rec(prop_conv, ns,
-      to_typecast_expr(src_original).op(), to_typecast_expr(src_ssa).op());
+    tmp.op() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      to_typecast_expr(src_original).op(),
+      to_typecast_expr(src_ssa).op());
     return std::move(tmp);
   }
   else if(id==ID_byte_extract_little_endian ||
@@ -94,7 +104,7 @@ static exprt build_full_lhs_rec(
   {
     byte_extract_exprt tmp = to_byte_extract_expr(src_original);
     tmp.op() = build_full_lhs_rec(
-      prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
+      decision_procedure, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
 
     // re-write into big case-split
   }
@@ -169,7 +179,8 @@ static void update_internal_field(
 
 /// Replace nondet values that appear in \p type by their values as found by
 /// \p solver.
-static void replace_nondet_in_type(typet &type, const prop_convt &solver)
+static void
+replace_nondet_in_type(typet &type, const decision_proceduret &solver)
 {
   if(type.id() == ID_array)
   {
@@ -182,7 +193,8 @@ static void replace_nondet_in_type(typet &type, const prop_convt &solver)
 
 /// Replace nondet values that appear in the type of \p expr and its
 /// subexpressions type by their values as found by \p solver.
-static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
+static void
+replace_nondet_in_type(exprt &expr, const decision_proceduret &solver)
 {
   replace_nondet_in_type(expr.type(), solver);
   for(auto &sub : expr.operands())
@@ -192,7 +204,7 @@ static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
 void build_goto_trace(
   const symex_target_equationt &target,
   ssa_step_predicatet is_last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
@@ -218,14 +230,14 @@ void build_goto_trace(
   {
     if(
       last_step_to_keep == target.SSA_steps.end() &&
-      is_last_step_to_keep(it, prop_conv))
+      is_last_step_to_keep(it, decision_procedure))
     {
       last_step_to_keep = it;
     }
 
     const SSA_stept &SSA_step = *it;
 
-    if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
+    if(decision_procedure.l_get(SSA_step.guard_literal) != tvt(true))
       continue;
 
     if(it->is_constraint() ||
@@ -250,7 +262,7 @@ void build_goto_trace(
         // these are just used to get the time stamp -- the clock type is
         // computed to be of the minimal necessary size, but we don't need to
         // know it to get the value so just use typeless
-        exprt clock_value = prop_conv.get(
+        exprt clock_value = decision_procedure.get(
           symbol_exprt::typeless(partial_order_concurrencyt::rw_clock_id(it)));
 
         const auto cv = numeric_cast<mp_integer>(clock_value);
@@ -342,7 +354,7 @@ void build_goto_trace(
       goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
       for(auto &arg : goto_trace_step.function_arguments)
-        arg = prop_conv.get(arg);
+        arg = decision_procedure.get(arg);
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);
@@ -359,15 +371,20 @@ void build_goto_trace(
       if(SSA_step.original_full_lhs.is_not_nil())
       {
         goto_trace_step.full_lhs = build_full_lhs_rec(
-          prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
-        replace_nondet_in_type(goto_trace_step.full_lhs, prop_conv);
+          decision_procedure,
+          ns,
+          SSA_step.original_full_lhs,
+          SSA_step.ssa_full_lhs);
+        replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
       }
 
       if(SSA_step.ssa_full_lhs.is_not_nil())
       {
-        goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);
+        goto_trace_step.full_lhs_value =
+          decision_procedure.get(SSA_step.ssa_full_lhs);
         simplify(goto_trace_step.full_lhs_value, ns);
-        replace_nondet_in_type(goto_trace_step.full_lhs_value, prop_conv);
+        replace_nondet_in_type(
+          goto_trace_step.full_lhs_value, decision_procedure);
       }
 
       for(const auto &j : SSA_step.converted_io_args)
@@ -378,7 +395,7 @@ void build_goto_trace(
         }
         else
         {
-          exprt tmp = prop_conv.get(j);
+          exprt tmp = decision_procedure.get(j);
           goto_trace_step.io_args.push_back(tmp);
         }
       }
@@ -388,7 +405,7 @@ void build_goto_trace(
         goto_trace_step.cond_expr = SSA_step.cond_expr;
 
         goto_trace_step.cond_value =
-          prop_conv.l_get(SSA_step.cond_literal).is_true();
+          decision_procedure.l_get(SSA_step.cond_literal).is_true();
       }
 
       if(ssa_step_it == last_step_to_keep)
@@ -400,31 +417,33 @@ void build_goto_trace(
 void build_goto_trace(
   const symex_target_equationt &target,
   symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
-  const auto is_last_step_to_keep = [last_step_to_keep](
-    symex_target_equationt::SSA_stepst::const_iterator it, const prop_convt &) {
-    return last_step_to_keep == it;
-  };
+  const auto is_last_step_to_keep =
+    [last_step_to_keep](
+      symex_target_equationt::SSA_stepst::const_iterator it,
+      const decision_proceduret &) { return last_step_to_keep == it; };
 
   return build_goto_trace(
-    target, is_last_step_to_keep, prop_conv, ns, goto_trace);
+    target, is_last_step_to_keep, decision_procedure, ns, goto_trace);
 }
 
 static bool is_failed_assertion_step(
   symex_target_equationt::SSA_stepst::const_iterator step,
-  const prop_convt &prop_conv)
+  const decision_proceduret &decision_procedure)
 {
-  return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false();
+  return step->is_assert() &&
+         decision_procedure.l_get(step->cond_literal).is_false();
 }
 
 void build_goto_trace(
   const symex_target_equationt &target,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
-  build_goto_trace(target, is_failed_assertion_step, prop_conv, ns, goto_trace);
+  build_goto_trace(
+    target, is_failed_assertion_step, decision_procedure, ns, goto_trace);
 }
diff --git a/src/goto-symex/build_goto_trace.h b/src/goto-symex/build_goto_trace.h
index e1006b3b604..bac90da760e 100644
--- a/src/goto-symex/build_goto_trace.h
+++ b/src/goto-symex/build_goto_trace.h
@@ -20,12 +20,12 @@ Date: July 2005
 /// Build a trace by going through the steps of \p target and stopping at the
 /// first failing assertion
 /// \param target: SSA form of the program
-/// \param prop_conv: solver from which to get valuations
+/// \param decision_procedure: solver from which to get valuations
 /// \param ns: namespace
 /// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace);
 
@@ -33,18 +33,19 @@ void build_goto_trace(
 /// the given step
 /// \param target: SSA form of the program
 /// \param last_step_to_keep: iterator pointing to the last step to keep
-/// \param prop_conv: solver from which to get valuations
+/// \param decision_procedure: solver from which to get valuations
 /// \param ns: namespace
 /// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
   symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace);
 
-typedef std::function<
-  bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)>
+typedef std::function<bool(
+  symex_target_equationt::SSA_stepst::const_iterator,
+  const decision_proceduret &)>
   ssa_step_predicatet;
 
 /// Build a trace by going through the steps of \p target and stopping after
@@ -52,13 +53,13 @@ typedef std::function<
 /// \param target: SSA form of the program
 /// \param stop_after_predicate: function with an SSA step iterator and solver
 ///   as argument, which should return true for the last step to keep
-/// \param prop_conv: solver from which to get valuations
+/// \param decision_procedure: solver from which to get valuations
 /// \param ns: namespace
 /// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
   ssa_step_predicatet stop_after_predicate,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace);
 
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 9eb7d711071..a98bd8a5d55 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -18,9 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/unwrap_nested_exception.h>
 
 #include <solvers/flattening/bv_conversion_exceptions.h>
+#include <solvers/prop/decision_procedure.h>
 #include <solvers/prop/literal_expr.h>
-#include <solvers/prop/prop.h>
-#include <solvers/prop/prop_conv.h>
 
 #include "equation_conversion_exceptions.h"
 #include "goto_symex_state.h"
@@ -329,20 +328,19 @@ void symex_target_equationt::constraint(
   merge_ireps(SSA_step);
 }
 
-void symex_target_equationt::convert(
-  prop_convt &prop_conv)
+void symex_target_equationt::convert(decision_proceduret &decision_procedure)
 {
   try
   {
-    convert_guards(prop_conv);
-    convert_assignments(prop_conv);
-    convert_decls(prop_conv);
-    convert_assumptions(prop_conv);
-    convert_assertions(prop_conv);
-    convert_goto_instructions(prop_conv);
-    convert_function_calls(prop_conv);
-    convert_io(prop_conv);
-    convert_constraints(prop_conv);
+    convert_guards(decision_procedure);
+    convert_assignments(decision_procedure);
+    convert_decls(decision_procedure);
+    convert_assumptions(decision_procedure);
+    convert_assertions(decision_procedure);
+    convert_goto_instructions(decision_procedure);
+    convert_function_calls(decision_procedure);
+    convert_io(decision_procedure);
+    convert_constraints(decision_procedure);
   }
   catch(const equation_conversion_exceptiont &conversion_exception)
   {
@@ -370,7 +368,8 @@ void symex_target_equationt::convert_assignments(
   }
 }
 
-void symex_target_equationt::convert_decls(prop_convt &prop_conv)
+void symex_target_equationt::convert_decls(
+  decision_proceduret &decision_procedure)
 {
   for(auto &step : SSA_steps)
   {
@@ -380,7 +379,7 @@ void symex_target_equationt::convert_decls(prop_convt &prop_conv)
       // the satisfiability of the formula.
       try
       {
-        prop_conv.convert(step.cond_expr);
+        decision_procedure.convert(step.cond_expr);
         step.converted = true;
       }
       catch(const bitvector_conversion_exceptiont &)
@@ -394,7 +393,7 @@ void symex_target_equationt::convert_decls(prop_convt &prop_conv)
 }
 
 void symex_target_equationt::convert_guards(
-  prop_convt &prop_conv)
+  decision_proceduret &decision_procedure)
 {
   for(auto &step : SSA_steps)
   {
@@ -409,7 +408,7 @@ void symex_target_equationt::convert_guards(
 
       try
       {
-        step.guard_literal = prop_conv.convert(step.guard);
+        step.guard_literal = decision_procedure.convert(step.guard);
       }
       catch(const bitvector_conversion_exceptiont &)
       {
@@ -422,7 +421,7 @@ void symex_target_equationt::convert_guards(
 }
 
 void symex_target_equationt::convert_assumptions(
-  prop_convt &prop_conv)
+  decision_proceduret &decision_procedure)
 {
   for(auto &step : SSA_steps)
   {
@@ -440,7 +439,7 @@ void symex_target_equationt::convert_assumptions(
 
         try
         {
-          step.cond_literal = prop_conv.convert(step.cond_expr);
+          step.cond_literal = decision_procedure.convert(step.cond_expr);
         }
         catch(const bitvector_conversion_exceptiont &)
         {
@@ -454,7 +453,7 @@ void symex_target_equationt::convert_assumptions(
 }
 
 void symex_target_equationt::convert_goto_instructions(
-  prop_convt &prop_conv)
+  decision_proceduret &decision_procedure)
 {
   for(auto &step : SSA_steps)
   {
@@ -472,7 +471,7 @@ void symex_target_equationt::convert_goto_instructions(
 
         try
         {
-          step.cond_literal = prop_conv.convert(step.cond_expr);
+          step.cond_literal = decision_procedure.convert(step.cond_expr);
         }
         catch(const bitvector_conversion_exceptiont &)
         {
@@ -512,7 +511,7 @@ void symex_target_equationt::convert_constraints(
 }
 
 void symex_target_equationt::convert_assertions(
-  prop_convt &prop_conv)
+  decision_proceduret &decision_procedure)
 {
   // we find out if there is only _one_ assertion,
   // which allows for a simpler formula
@@ -533,12 +532,12 @@ void symex_target_equationt::convert_assertions(
       if(step.is_assert() && !step.ignore && !step.converted)
       {
         step.converted = true;
-        prop_conv.set_to_false(step.cond_expr);
+        decision_procedure.set_to_false(step.cond_expr);
         step.cond_literal=const_literal(false);
         return; // prevent further assumptions!
       }
       else if(step.is_assume())
-        prop_conv.set_to_true(step.cond_expr);
+        decision_procedure.set_to_true(step.cond_expr);
     }
 
     UNREACHABLE; // unreachable
@@ -573,7 +572,7 @@ void symex_target_equationt::convert_assertions(
       // do the conversion
       try
       {
-        step.cond_literal = prop_conv.convert(implication);
+        step.cond_literal = decision_procedure.convert(implication);
       }
       catch(const bitvector_conversion_exceptiont &)
       {
@@ -598,7 +597,7 @@ void symex_target_equationt::convert_assertions(
   }
 
   // the below is 'true' if there are no assertions
-  prop_conv.set_to_true(disjunction(disjuncts));
+  decision_procedure.set_to_true(disjunction(disjuncts));
 }
 
 void symex_target_equationt::convert_function_calls(
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index 0776967602f..045fca809a3 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -32,7 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class decision_proceduret;
 class namespacet;
-class prop_convt;
+class decision_proceduret;
 
 /// Inheriting the interface of symex_targett this class represents the SSA
 /// form of the input program as a list of \ref SSA_stept. It further extends
@@ -176,51 +176,57 @@ class symex_target_equationt:public symex_targett
   /// Interface method to initiate the conversion into a decision procedure
   /// format. The method iterates over the equation, i.e. over the SSA steps and
   /// converts each type of step separately.
-  /// \param prop_conv: A handle to a particular decision procedure interface
-  void convert(prop_convt &prop_conv);
+  /// \param decision_procedure: A handle to a particular decision procedure
+  ///   interface
+  void convert(decision_proceduret &decision_procedure);
 
   /// Converts assignments: set the equality _lhs==rhs_ to _True_.
   /// \param decision_procedure: A handle to a particular decision procedure
-  ///  interface
+  ///   interface
   void convert_assignments(decision_proceduret &decision_procedure);
 
   /// Converts declarations: these are effectively ignored by the decision
   /// procedure.
-  /// \param prop_conv: A handle to a particular decision procedure interface
-  void convert_decls(prop_convt &prop_conv);
+  /// \param decision_procedure: A handle to a particular decision procedure
+  ///   interface
+  void convert_decls(decision_proceduret &decision_procedure);
 
   /// Converts assumptions: convert the expression the assumption represents.
-  /// \param prop_conv: A handle to a particular decision procedure interface
-  void convert_assumptions(prop_convt &prop_conv);
+  /// \param decision_procedure: A handle to a particular decision procedure
+  ///   interface
+  void convert_assumptions(decision_proceduret &decision_procedure);
 
   /// Converts assertions: build a disjunction of negated assertions.
-  /// \param prop_conv: A handle to a particular decision procedure interface
-  void convert_assertions(prop_convt &prop_conv);
+  /// \param decision_procedure: A handle to a particular decision procedure
+  ///   interface
+  void convert_assertions(decision_proceduret &decision_procedure);
 
   /// Converts constraints: set the represented condition to _True_.
   /// \param decision_procedure: A handle to a particular decision procedure
-  ///  interface
+  ///   interface
   void convert_constraints(decision_proceduret &decision_procedure);
 
   /// Converts goto instructions: convert the expression representing the
   /// condition of this goto.
-  /// \param prop_conv: A handle to a particular decision procedure interface
-  void convert_goto_instructions(prop_convt &prop_conv);
+  /// \param decision_procedure: A handle to a particular decision procedure
+  ///   interface
+  void convert_goto_instructions(decision_proceduret &decision_procedure);
 
   /// Converts guards: convert the expression the guard represents.
-  /// \param prop_conv: A handle to a particular decision procedure interface
-  void convert_guards(prop_convt &prop_conv);
+  /// \param decision_procedure: A handle to a particular decision procedure
+  ///   interface
+  void convert_guards(decision_proceduret &decision_procedure);
 
   /// Converts function calls: for each argument build an equality between its
   /// symbol and the argument itself.
   /// \param decision_procedure: A handle to a particular decision procedure
-  ///  interface
+  ///   interface
   void convert_function_calls(decision_proceduret &decision_procedure);
 
   /// Converts I/O: for each argument build an equality between its
   /// symbol and the argument itself.
   /// \param decision_procedure: A handle to a particular decision procedure
-  ///  interface
+  ///   interface
   void convert_io(decision_proceduret &decision_procedure);
 
   exprt make_expression() const;
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 81a435735cb..161afa4385f 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -145,10 +145,10 @@ SRC = $(BOOLEFORCE_SRC) \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \
       prop/decision_procedure.cpp \
+      prop/decision_procedure_incremental.cpp \
       prop/literal.cpp \
       prop/prop_minimize.cpp \
       prop/prop.cpp \
-      prop/prop_conv.cpp \
       prop/prop_conv_solver.cpp \
       qbf/qbf_quantor.cpp \
       qbf/qbf_qube.cpp \
diff --git a/src/solvers/README.md b/src/solvers/README.md
index 1909f3e9c3b..4b9dc66513a 100644
--- a/src/solvers/README.md
+++ b/src/solvers/README.md
@@ -56,9 +56,11 @@ getting an over-view of the solvers currently supported.
 
 Many (but not all) decision procedures have a notion of logical
 expression and can provide information about logical expressions
-within the solver.  `prop_convt` expands on the interface of
-`decision_proceduret` to add a data-type (`literalt`) and interfaces
-for manipulating logical expressions within the solver.
+within the solver.  `decision_proceduret` also has functions to
+get a handle (in the form of a `literalt`) on a particular
+Boolean expression within the solver, which is useful the
+retrieve to easily the truth value of that expression from
+a satisfying assignment.
 
 Within decision procedures it is common to reduce the logical
 expressions to equivalent expressions in a simpler language.  This is
@@ -75,7 +77,7 @@ processors, creating a good SAT solver is a very specialised skill, so
 CPROVER uses third-party SAT solvers.  By default this is MiniSAT, but
 others are supported (see the `sat/` directory).  To do this it needs a
 software interface to a SAT solver : this is `propt`.  It uses the
-same `literalt` to refer to Boolean variables, just as `prop_convt`
+same `literalt` to refer to Boolean variables, just as `decision_proceduret`
 uses them to refer to logical expressions.  `land`, `lor`, `lxor` and
 so on allow gates to be constructed to express the formulae to be
 solved.  If `cnf_handled_well` is true then you may also use `lcnf` to
@@ -83,7 +85,7 @@ build formulae.  Finally, `prop_solve` will run the decision procedure.
 
 As previously mentioned, many decision procedures reduce formulae to
 CNF and solve with a SAT solver.  `prop_conv_solvert` contains the
-foundations of this conversion.  It implements the `prop_convt` by
+foundations of this conversion.  It implements the `decision_proceduret` by
 having an instance of `propt` (a SAT solver) and reducing the
 expressions that are input into CNF.  The key entry point to this
 procedure is `prop_conv_solvert::convert` which then splits into
diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp
index 2588275b14f..92009bb6aad 100644
--- a/src/solvers/flattening/functions.cpp
+++ b/src/solvers/flattening/functions.cpp
@@ -66,7 +66,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/flattening/functions.h b/src/solvers/flattening/functions.h
index fe2018ef12e..abf9e66c960 100644
--- a/src/solvers/flattening/functions.h
+++ b/src/solvers/flattening/functions.h
@@ -12,17 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
 #define CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
 
+#include <map>
 #include <set>
 
 #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)
+  {
+  }
 
   virtual ~functionst()
   {
@@ -37,7 +40,7 @@ class functionst
   }
 
 protected:
-  prop_convt &prop_conv;
+  decision_proceduret &decision_procedure;
 
   typedef std::set<function_application_exprt> applicationst;
 
diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp
index 5099e81f80c..9e3b78dfcf5 100644
--- a/src/solvers/prop/cover_goals.cpp
+++ b/src/solvers/prop/cover_goals.cpp
@@ -13,8 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/message.h>
 
+#include "decision_procedure_incremental.h"
 #include "literal_expr.h"
-#include "prop_conv.h"
 
 cover_goalst::~cover_goalst()
 {
@@ -28,8 +28,9 @@ void cover_goalst::mark()
     o->satisfying_assignment();
 
   for(auto &g : goals)
-    if(g.status==goalt::statust::UNKNOWN &&
-       prop_conv.l_get(g.condition).is_true())
+    if(
+      g.status == goalt::statust::UNKNOWN &&
+      decision_procedure.l_get(g.condition).is_true())
     {
       g.status=goalt::statust::COVERED;
       _number_covered++;
@@ -56,7 +57,7 @@ void cover_goalst::constraint()
       disjuncts.push_back(literal_exprt(g_it->condition));
 
   // this is 'false' if there are no disjuncts
-  prop_conv.set_to_true(disjunction(disjuncts));
+  decision_procedure.set_to_true(disjunction(disjuncts));
 }
 
 /// Build clause
@@ -67,7 +68,7 @@ void cover_goalst::freeze_goal_variables()
       g_it!=goals.end();
       g_it++)
     if(!g_it->condition.is_constant())
-      prop_conv.set_frozen(g_it->condition);
+      decision_procedure.set_frozen(g_it->condition);
 }
 
 /// Try to cover all goals
@@ -88,7 +89,7 @@ operator()(message_handlert &message_handler)
     _iterations++;
 
     constraint();
-    dec_result = prop_conv();
+    dec_result = decision_procedure();
 
     switch(dec_result)
     {
diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h
index 8c4593313a2..62e197f7e07 100644
--- a/src/solvers/prop/cover_goals.h
+++ b/src/solvers/prop/cover_goals.h
@@ -14,21 +14,21 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <list>
 
-#include "decision_procedure.h"
+#include "decision_procedure_incremental.h"
 #include "literal.h"
 
 class message_handlert;
-class prop_convt;
+class decision_proceduret;
 
 /// Try to cover some given set of goals incrementally. This can be seen as a
 /// heuristic variant of SAT-based set-cover. No minimality guarantee.
 class cover_goalst
 {
 public:
-  explicit cover_goalst(prop_convt &_prop_conv):
-    _number_covered(0),
-    _iterations(0),
-    prop_conv(_prop_conv)
+  explicit cover_goalst(decision_procedure_incrementalt &_decision_procedure)
+    : _number_covered(0),
+      _iterations(0),
+      decision_procedure(_decision_procedure)
   {
   }
 
@@ -95,7 +95,7 @@ class cover_goalst
 protected:
   std::size_t _number_covered;
   unsigned _iterations;
-  prop_convt &prop_conv;
+  decision_procedure_incrementalt &decision_procedure;
 
   typedef std::vector<observert *> observerst;
   observerst observers;
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/decision_procedure_incremental.cpp
similarity index 58%
rename from src/solvers/prop/prop_conv.cpp
rename to src/solvers/prop/decision_procedure_incremental.cpp
index b371aa37e21..5f2f4c57b13 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/decision_procedure_incremental.cpp
@@ -6,27 +6,27 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include "prop_conv.h"
+#include "decision_procedure_incremental.h"
 #include <algorithm>
 
 /// determine whether a variable is in the final conflict
-bool prop_convt::is_in_conflict(literalt) const
+bool decision_procedure_incrementalt::is_in_conflict(literalt) const
 {
   UNREACHABLE;
   return false;
 }
 
-void prop_convt::set_assumptions(const bvt &)
+void decision_procedure_incrementalt::set_assumptions(const bvt &)
 {
   UNREACHABLE;
 }
 
-void prop_convt::set_frozen(const literalt)
+void decision_procedure_incrementalt::set_frozen(const literalt)
 {
   UNREACHABLE;
 }
 
-void prop_convt::set_frozen(const bvt &bv)
+void decision_procedure_incrementalt::set_frozen(const bvt &bv)
 {
   for(const auto &bit : bv)
     if(!bit.is_constant())
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/decision_procedure_incremental.h
similarity index 65%
rename from src/solvers/prop/prop_conv.h
rename to src/solvers/prop/decision_procedure_incremental.h
index f65ce436043..a500d7c3fc2 100644
--- a/src/solvers/prop/prop_conv.h
+++ b/src/solvers/prop/decision_procedure_incremental.h
@@ -6,12 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H
+#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H
 
-#ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
-#define CPROVER_SOLVERS_PROP_PROP_CONV_H
-
-#include <string>
 #include <map>
+#include <string>
 
 #include <util/expr.h>
 #include <util/message.h>
@@ -25,10 +24,12 @@ Author: Daniel Kroening, kroening@kroening.com
 // API that provides a "handle" in the form of a literalt
 // for expressions.
 
-class prop_convt:public decision_proceduret
+class decision_procedure_incrementalt : public decision_proceduret
 {
 public:
-  virtual ~prop_convt() { }
+  virtual ~decision_procedure_incrementalt()
+  {
+  }
 
   using decision_proceduret::operator();
 
@@ -36,12 +37,20 @@ class prop_convt:public decision_proceduret
   virtual void set_frozen(literalt a);
   virtual void set_frozen(const bvt &);
   virtual void set_assumptions(const bvt &_assumptions);
-  virtual bool has_set_assumptions() const { return false; }
-  virtual void set_all_frozen() {}
+  virtual bool has_set_assumptions() const
+  {
+    return false;
+  }
+  virtual void set_all_frozen()
+  {
+  }
 
   // returns true if an assumption is in the final conflict
   virtual bool is_in_conflict(literalt l) const;
-  virtual bool has_is_in_conflict() const { return false; }
+  virtual bool has_is_in_conflict() const
+  {
+    return false;
+  }
 };
 
 //
@@ -49,4 +58,4 @@ class prop_convt:public decision_proceduret
 // propositional skeleton by passing it to a propt
 //
 
-#endif // CPROVER_SOLVERS_PROP_PROP_CONV_H
+#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_INCREMENTAL_H
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
index b0600ad1ded..c46a7f40c4a 100644
--- a/src/solvers/prop/prop_conv_solver.h
+++ b/src/solvers/prop/prop_conv_solver.h
@@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 #include <util/std_expr.h>
 
-#include "decision_procedure.h"
+#include "decision_procedure_incremental.h"
 #include "literal.h"
 #include "literal_expr.h"
 #include "prop.h"
-#include "prop_conv.h"
 #include "solver_resource_limits.h"
 
-class prop_conv_solvert : public prop_convt, public solver_resource_limitst
+class prop_conv_solvert : public decision_procedure_incrementalt,
+                          public solver_resource_limitst
 {
 public:
   prop_conv_solvert(propt &_prop, message_handlert &message_handler)
@@ -43,8 +43,8 @@ class prop_conv_solvert : public prop_convt, public solver_resource_limitst
   }
   exprt get(const exprt &expr) const override;
 
-  // overloading from prop_convt
-  using prop_convt::set_frozen;
+  // overloading from decision_proceduret
+  using decision_procedure_incrementalt::set_frozen;
   tvt l_get(literalt a) const override
   {
     return prop.l_get(a);
diff --git a/src/solvers/prop/prop_minimize.cpp b/src/solvers/prop/prop_minimize.cpp
index eb3bf9e6f9c..a40e4ce0446 100644
--- a/src/solvers/prop/prop_minimize.cpp
+++ b/src/solvers/prop/prop_minimize.cpp
@@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "literal_expr.h"
 
 prop_minimizet::prop_minimizet(
-  prop_convt &_prop_conv,
+  decision_procedure_incrementalt &_decision_procedure,
   message_handlert &message_handler)
-  : prop_conv(_prop_conv), log(message_handler)
+  : decision_procedure(_decision_procedure), log(message_handler)
 {
 }
 
@@ -47,11 +47,12 @@ void prop_minimizet::fix_objectives()
       o_it != entry.end();
       ++o_it)
   {
-    if(!o_it->fixed && prop_conv.l_get(o_it->condition).is_false())
+    if(!o_it->fixed && decision_procedure.l_get(o_it->condition).is_false())
     {
       _number_satisfied++;
       _value += current->first;
-      prop_conv.set_to(literal_exprt(o_it->condition), false); // fix it
+      decision_procedure.set_to(
+        literal_exprt(o_it->condition), false); // fix it
       o_it->fixed = true;
       found = true;
     }
@@ -88,7 +89,7 @@ literalt prop_minimizet::constraint()
     forall_literals(it, or_clause)
       disjuncts.push_back(literal_exprt(*it));
 
-    return prop_conv.convert(disjunction(disjuncts));
+    return decision_procedure.convert(disjunction(disjuncts));
   }
 }
 
@@ -96,7 +97,7 @@ literalt prop_minimizet::constraint()
 void prop_minimizet::operator()()
 {
   // we need to use assumptions
-  PRECONDITION(prop_conv.has_set_assumptions());
+  PRECONDITION(decision_procedure.has_set_assumptions());
 
   _iterations = 0;
   _number_satisfied = 0;
@@ -122,8 +123,8 @@ void prop_minimizet::operator()()
 
         bvt assumptions;
         assumptions.push_back(c);
-        prop_conv.set_assumptions(assumptions);
-        dec_result = prop_conv();
+        decision_procedure.set_assumptions(assumptions);
+        dec_result = decision_procedure();
 
         switch(dec_result)
         {
@@ -151,7 +152,7 @@ void prop_minimizet::operator()()
     // Run solver again to get one.
 
     bvt assumptions; // no assumptions
-    prop_conv.set_assumptions(assumptions);
-    (void)prop_conv();
+    decision_procedure.set_assumptions(assumptions);
+    (void)decision_procedure();
   }
 }
diff --git a/src/solvers/prop/prop_minimize.h b/src/solvers/prop/prop_minimize.h
index de3d730398f..5336d465174 100644
--- a/src/solvers/prop/prop_minimize.h
+++ b/src/solvers/prop/prop_minimize.h
@@ -16,14 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/message.h>
 
-#include "prop_conv.h"
+#include "decision_procedure_incremental.h"
 
 /// Computes a satisfying assignment of minimal cost according to a const
 /// function using incremental SAT
 class prop_minimizet
 {
 public:
-  prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler);
+  prop_minimizet(decision_procedure_incrementalt &, message_handlert &);
 
   void operator()();
 
@@ -71,7 +71,7 @@ class prop_minimizet
   std::size_t _number_satisfied = 0;
   std::size_t _number_objectives = 0;
   weightt _value = 0;
-  prop_convt &prop_conv;
+  decision_procedure_incrementalt &decision_procedure;
   messaget log;
 
   literalt constraint();
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
index 774df1f4adf..94dfc136388 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/src/solvers/smt2/smt2_conv.h
@@ -20,9 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/irep_hash_container.h>
 #endif
 
-#include <solvers/prop/prop_conv.h>
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
+#include <solvers/prop/decision_procedure_incremental.h>
 
 #include "letify.h"
 
@@ -31,7 +31,7 @@ class constant_exprt;
 class index_exprt;
 class member_exprt;
 
-class smt2_convt:public prop_convt
+class smt2_convt : public decision_procedure_incrementalt
 {
 public:
   enum class solvert