diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index e39bbede197..d6ce7f48bd8 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -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.get(step->cond_handle).is_false();
   };
 }
 
@@ -103,19 +103,6 @@ void output_error_trace(
   }
 }
 
-void freeze_guards(
-  const symex_target_equationt &equation,
-  prop_convt &prop_conv)
-{
-  for(const auto &step : equation.SSA_steps)
-  {
-    if(!step.guard_literal.is_constant())
-      prop_conv.set_frozen(step.guard_literal);
-    if(step.is_assert() && !step.cond_literal.is_constant())
-      prop_conv.set_frozen(step.cond_literal);
-  }
-}
-
 /// outputs an error witness in graphml format
 void output_graphml(
   const goto_tracet &goto_trace,
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 6c39c116ed0..5591c4ff102 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -60,8 +60,6 @@ void output_error_trace(
   const trace_optionst &,
   ui_message_handlert &);
 
-void freeze_guards(const symex_target_equationt &, prop_convt &);
-
 void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
 void output_graphml(
   const symex_target_equationt &,
diff --git a/src/goto-checker/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp
index 2f35b90bdea..1365ec76387 100644
--- a/src/goto-checker/counterexample_beautification.cpp
+++ b/src/goto-checker/counterexample_beautification.cpp
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol.h>
 #include <util/threeval.h>
 
-#include <solvers/prop/literal_expr.h>
 #include <solvers/prop/prop_minimize.h>
 
 counterexample_beautificationt::counterexample_beautificationt(
@@ -41,7 +40,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(!prop_conv.get(it->guard_handle).is_false())
       {
         const typet &type = it->ssa_lhs.type();
 
@@ -78,10 +77,14 @@ counterexample_beautificationt::get_failed_property(
         equation.SSA_steps.begin();
       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() && prop_conv.get(it->guard_handle).is_true() &&
+      prop_conv.get(it->cond_handle).is_false())
+    {
       return it;
+    }
+  }
 
   UNREACHABLE;
   return equation.SSA_steps.end();
@@ -95,7 +98,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
   failed = get_failed_property(boolbv, equation);
 
   // lock the failed assertion
-  boolbv.set_to(literal_exprt(failed->cond_literal), false);
+  boolbv.set_to(failed->cond_handle, false);
 
   {
     log.status() << "Beautifying counterexample (guards)" << messaget::eom;
@@ -113,8 +116,9 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
         it->is_assignment() &&
         it->assignment_type != symex_targett::assignment_typet::HIDDEN)
       {
-        if(!it->guard_literal.is_constant())
-          guard_count[it->guard_literal]++;
+        literalt l = boolbv.convert(it->guard_handle);
+        if(!l.is_constant())
+          guard_count[l]++;
       }
 
       // reached failed assertion?
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
index 9f59452f306..77fc01e7e2c 100644
--- a/src/goto-checker/goto_symex_fault_localizer.cpp
+++ b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -58,10 +58,11 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(
       step.assignment_type == symex_targett::assignment_typet::STATE &&
       !step.ignore)
     {
-      if(!step.guard_literal.is_constant())
+      literalt l = solver.convert(step.guard_handle);
+      if(!l.is_constant())
       {
         auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
-        localization_points.emplace(step.guard_literal, emplace_result.first);
+        localization_points.emplace(l, emplace_result.first);
       }
     }
 
@@ -90,7 +91,7 @@ bool goto_symex_fault_localizert::check(
   }
 
   // lock the failed assertion
-  assumptions.push_back(!failed_step.cond_literal);
+  assumptions.push_back(!solver.convert(failed_step.cond_handle));
 
   solver.set_assumptions(assumptions);
 
diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/src/goto-checker/goto_symex_fault_localizer.h
index 4d96eb2e703..9f5e6ebd64c 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/prop_conv.h>
+
 #include "fault_localization_provider.h"
 
 class goto_symex_fault_localizert
diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp
index 0a2e7ce65a9..bbd110fd25d 100644
--- a/src/goto-checker/goto_symex_property_decider.cpp
+++ b/src/goto-checker/goto_symex_property_decider.cpp
@@ -36,7 +36,7 @@ exprt goto_symex_property_decidert::goalt::as_expr() const
   exprt::operandst conjuncts;
   conjuncts.reserve(instances.size());
   for(const auto &inst : instances)
-    conjuncts.push_back(literal_exprt(inst->cond_literal));
+    conjuncts.push_back(inst->cond_handle);
   return conjunction(conjuncts);
 }
 
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp
index 8ec7a52adfd..7d27d010fbe 100644
--- a/src/goto-checker/multi_path_symex_checker.cpp
+++ b/src/goto-checker/multi_path_symex_checker.cpp
@@ -72,9 +72,6 @@ multi_path_symex_checkert::prepare_property_decider(propertiest &properties)
   std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
     properties, equation, property_decider, ui_message_handler);
 
-  if(options.get_bool_option("localize-faults"))
-    freeze_guards(equation, property_decider.get_solver());
-
   return solver_runtime;
 }
 
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index e8b68012bcd..60be0403b6e 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/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.get(SSA_step.guard_handle).is_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.get(SSA_step.cond_handle).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.get(step->cond_handle).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/ssa_step.h b/src/goto-symex/ssa_step.h
index 6d2262e6daf..386c1adac2d 100644
--- a/src/goto-symex/ssa_step.h
+++ b/src/goto-symex/ssa_step.h
@@ -10,7 +10,6 @@ Author: Romain Brenguier <romain.brenguier@diffblue.com>
 #define CPROVER_GOTO_SYMEX_SSA_STEP_H
 
 #include <goto-programs/goto_trace.h>
-#include <solvers/prop/literal.h>
 
 #include "symex_target.h"
 
@@ -35,7 +34,7 @@ Author: Romain Brenguier <romain.brenguier@diffblue.com>
 /// which represent the condition guarding this step, i.e. what must hold for
 /// this step to be taken. Both `guard` and `cond_expr` will later be
 /// translated into verification condition for the SAT/SMT solver (or some
-/// other decision procedure), to be referred by their respective literals.
+/// other decision procedure), to be referred by their respective handles.
 /// Constraints usually arise from external conditions, such as memory models
 /// or partial orders: they represent assumptions with global effect.
 ///
@@ -136,7 +135,7 @@ class SSA_stept
   bool hidden = false;
 
   exprt guard;
-  literalt guard_literal;
+  exprt guard_handle;
 
   // for ASSIGNMENT and DECL
   ssa_exprt ssa_lhs;
@@ -146,7 +145,7 @@ class SSA_stept
 
   // for ASSUME/ASSERT/GOTO/CONSTRAINT
   exprt cond_expr;
-  literalt cond_literal;
+  exprt cond_handle;
   std::string comment;
 
   // for INPUT/OUTPUT
@@ -177,14 +176,14 @@ class SSA_stept
       type(_type),
       hidden(false),
       guard(static_cast<const exprt &>(get_nil_irep())),
-      guard_literal(const_literal(false)),
+      guard_handle(false_exprt()),
       ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
       ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
       original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
       ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
       assignment_type(symex_targett::assignment_typet::STATE),
       cond_expr(static_cast<const exprt &>(get_nil_irep())),
-      cond_literal(const_literal(false)),
+      cond_handle(false_exprt()),
       formatted(false),
       atomic_section_id(0),
       ignore(false)
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 9eb7d711071..c33cd895bd1 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -17,10 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/throw_with_nested.h>
 #include <util/unwrap_nested_exception.h>
 
+#include <solvers/decision_procedure.h>
 #include <solvers/flattening/bv_conversion_exceptions.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 +327,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 +367,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 +378,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.handle(step.cond_expr);
         step.converted = true;
       }
       catch(const bitvector_conversion_exceptiont &)
@@ -394,12 +392,12 @@ 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)
   {
     if(step.ignore)
-      step.guard_literal=const_literal(false);
+      step.guard_handle = false_exprt();
     else
     {
       log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
@@ -409,7 +407,7 @@ void symex_target_equationt::convert_guards(
 
       try
       {
-        step.guard_literal = prop_conv.convert(step.guard);
+        step.guard_handle = decision_procedure.handle(step.guard);
       }
       catch(const bitvector_conversion_exceptiont &)
       {
@@ -422,14 +420,14 @@ 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)
   {
     if(step.is_assume())
     {
       if(step.ignore)
-        step.cond_literal=const_literal(true);
+        step.cond_handle = true_exprt();
       else
       {
         log.conditional_output(
@@ -440,7 +438,7 @@ void symex_target_equationt::convert_assumptions(
 
         try
         {
-          step.cond_literal = prop_conv.convert(step.cond_expr);
+          step.cond_handle = decision_procedure.handle(step.cond_expr);
         }
         catch(const bitvector_conversion_exceptiont &)
         {
@@ -454,14 +452,14 @@ 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)
   {
     if(step.is_goto())
     {
       if(step.ignore)
-        step.cond_literal=const_literal(true);
+        step.cond_handle = true_exprt();
       else
       {
         log.conditional_output(
@@ -472,7 +470,7 @@ void symex_target_equationt::convert_goto_instructions(
 
         try
         {
-          step.cond_literal = prop_conv.convert(step.cond_expr);
+          step.cond_handle = decision_procedure.handle(step.cond_expr);
         }
         catch(const bitvector_conversion_exceptiont &)
         {
@@ -512,7 +510,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 +531,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);
-        step.cond_literal=const_literal(false);
+        decision_procedure.set_to_false(step.cond_expr);
+        step.cond_handle = false_exprt();
         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 +571,7 @@ void symex_target_equationt::convert_assertions(
       // do the conversion
       try
       {
-        step.cond_literal = prop_conv.convert(implication);
+        step.cond_handle = decision_procedure.handle(implication);
       }
       catch(const bitvector_conversion_exceptiont &)
       {
@@ -583,22 +581,21 @@ void symex_target_equationt::convert_assertions(
       }
 
       // store disjunct
-      disjuncts.push_back(literal_exprt(!step.cond_literal));
+      disjuncts.push_back(not_exprt(step.cond_handle));
     }
     else if(step.is_assume())
     {
       // the assumptions have been converted before
       // avoid deep nesting of ID_and expressions
       if(assumption.id()==ID_and)
-        assumption.copy_to_operands(literal_exprt(step.cond_literal));
+        assumption.copy_to_operands(step.cond_handle);
       else
-        assumption=
-          and_exprt(assumption, literal_exprt(step.cond_literal));
+        assumption = and_exprt(assumption, step.cond_handle);
     }
   }
 
   // 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..1106d1001f1 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -24,15 +24,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_trace.h>
 
-#include <solvers/prop/literal.h>
-
 #include "renaming_level.h"
 #include "ssa_step.h"
 #include "symex_target.h"
 
 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 +174,49 @@ 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 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
+  /// \param decision_procedure: A handle to a decision procedure
   ///  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 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 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 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
+  /// \param decision_procedure: A handle to a decision procedure 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 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 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
+  /// \param decision_procedure: A handle to a decision procedure 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
+  /// \param decision_procedure: A handle to a decision procedure interface
   void convert_io(decision_proceduret &decision_procedure);
 
   exprt make_expression() const;
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index f1998475f63..fdbd4194696 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -66,6 +66,10 @@ optionalt<bool> prop_conv_solvert::get_bool(const exprt &expr) const
 
     return prop.l_get(result->second).is_true();
   }
+  else if(expr.id() == ID_literal)
+  {
+    return prop.l_get(to_literal_expr(expr).get_literal()).is_true();
+  }
 
   // sub-expressions
 
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index d1c9919ebb9..b8fcdebb119 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -208,6 +208,24 @@ exprt smt2_convt::get(const exprt &expr) const
       return nil_exprt();
     return member_exprt(tmp, member_expr.get_component_name(), expr.type());
   }
+  else if(expr.id() == ID_literal)
+  {
+    auto l = to_literal_expr(expr).get_literal();
+    if(l_get(l).is_true())
+      return true_exprt();
+    else
+      return false_exprt();
+  }
+  else if(expr.id() == ID_not)
+  {
+    auto op = get(to_not_expr(expr).op());
+    if(op.is_true())
+      return false_exprt();
+    else if(op.is_false())
+      return true_exprt();
+  }
+  else if(expr.is_constant())
+    return expr;
 
   return nil_exprt();
 }