diff --git a/.travis.yml b/.travis.yml
index c62ee5db9ed..ffbfb288b96 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -201,7 +201,7 @@ jobs:
         - cmake --build build -- -j4
       script: (cd build; bin/unit "[core][irept]")
 
-    # cmake build using g++-7, enable CMAKE_USE_CUDD
+    # cmake build using g++-7, enable CMAKE_USE_CUDD and BDD_GUARDS
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -223,7 +223,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
diff --git a/COMPILING.md b/COMPILING.md
index 6ed73f03989..6eff98f9ff4 100644
--- a/COMPILING.md
+++ b/COMPILING.md
@@ -310,3 +310,22 @@ If compiling with cmake:
    ```
    cmake --build build
    ```
+
+## Use BDDs for guards
+
+There are two implementation for symex guards. The default one uses the
+internal representation of expression. The other one uses BDDs and
+though experimental, it is expected to have better performance,
+in particular when used in conjunction with CUDD.
+
+To use the BDD implementation of guards, add the `BDD_GUARDS`
+compilation flag:
+  * If compiling with make:
+    ```
+    make -C src CXXFLAGS="-O2 -DBDD_GUARDS"
+    ```
+  * If compiling with CMake:
+    ```
+    cmake -H. -Bbuild -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
+    ```
+    and then `cmake --build build`
diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt
index 561fe5ab0c7..a05181109f5 100644
--- a/jbmc/regression/jbmc/CMakeLists.txt
+++ b/jbmc/regression/jbmc/CMakeLists.txt
@@ -2,9 +2,18 @@ add_test_pl_tests(
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
-add_test_pl_profile(
-    "jbmc-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
-    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
-    "CORE"
-)
+if(DEFINED BDD_GUARDS)
+    add_test_pl_profile(
+            "jbmc-symex-driven-lazy-loading"
+            "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
+            "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
+            "CORE"
+    )
+else()
+    add_test_pl_profile(
+            "jbmc-symex-driven-lazy-loading"
+            "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
+            "-C;-X;symex-driven-lazy-loading-expected-failure;-X;bdd-expected-timeout;-s;symex-driven-loading"
+            "CORE"
+    )
+endif()
diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile
index e6541f77df2..aaf7efdf539 100644
--- a/jbmc/regression/jbmc/Makefile
+++ b/jbmc/regression/jbmc/Makefile
@@ -4,11 +4,19 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),)
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+else
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading
+endif
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),)
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+else
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading
+endif
 
 show:
 	@for dir in *; do \
diff --git a/jbmc/regression/jbmc/class-literals/test.desc b/jbmc/regression/jbmc/class-literals/test.desc
index a39e4029a74..47ca0a9496b 100644
--- a/jbmc/regression/jbmc/class-literals/test.desc
+++ b/jbmc/regression/jbmc/class-literals/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE bdd-expected-timeout
 Test.class
 --function Test.main
 ^EXIT=0$
@@ -6,3 +6,8 @@ Test.class
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test is deactivated for the build with BDDs because it takes more
+than 10 minutes for the test to complete.
+This is due to the size of the BDD representing the guards growing more than
+they do when represented as exprt.
diff --git a/src/analyses/CMakeLists.txt b/src/analyses/CMakeLists.txt
index 03be00fc8de..e030a507f63 100644
--- a/src/analyses/CMakeLists.txt
+++ b/src/analyses/CMakeLists.txt
@@ -3,4 +3,8 @@ add_library(analyses ${sources})
 
 generic_includes(analyses)
 
-target_link_libraries(analyses util pointer-analysis)
+if(CMAKE_USE_CUDD)
+    target_include_directories(analyses PUBLIC ${CUDD_INCLUDE}/cudd/)
+endif()
+
+target_link_libraries(analyses util pointer-analysis solvers)
diff --git a/src/analyses/Makefile b/src/analyses/Makefile
index dbab82bda96..3e52255c82e 100644
--- a/src/analyses/Makefile
+++ b/src/analyses/Makefile
@@ -12,6 +12,8 @@ SRC = ai.cpp \
       global_may_alias.cpp \
       goto_check.cpp \
       goto_rw.cpp \
+      guard_bdd.cpp \
+      guard_expr.cpp \
       interval_analysis.cpp \
       interval_domain.cpp \
       invariant_propagation.cpp \
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index cc4c0b76df8..84d131a2bef 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
-#include <util/guard.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
@@ -36,6 +35,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/remove_skip.h>
 
+#include "guard.h"
 #include "local_bitvector_analysis.h"
 
 class goto_checkt
@@ -84,6 +84,7 @@ class goto_checkt
   const namespacet &ns;
   std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
   goto_programt::const_targett current_target;
+  guard_managert guard_manager;
 
   void check_rec(
     const exprt &expr,
@@ -1650,7 +1651,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 
 void goto_checkt::check(const exprt &expr)
 {
-  guardt guard{true_exprt{}};
+  guardt guard{true_exprt{}, guard_manager};
   check_rec(expr, guard, false);
 }
 
@@ -1782,7 +1783,7 @@ void goto_checkt::goto_check(
             "pointer dereference",
             i.source_location,
             pointer,
-            guardt(true_exprt()));
+            guardt(true_exprt(), guard_manager));
         }
       }
 
@@ -1820,7 +1821,7 @@ void goto_checkt::goto_check(
           "pointer dereference",
           i.source_location,
           pointer,
-          guardt(true_exprt()));
+          guardt(true_exprt(), guard_manager));
       }
 
       // this has no successor
@@ -1897,7 +1898,7 @@ void goto_checkt::goto_check(
           "memory-leak",
           source_location,
           eq,
-          guardt(true_exprt()));
+          guardt(true_exprt(), guard_manager));
       }
     }
 
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index 49ce2de73c7..67667ea8c34 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -17,7 +17,7 @@ Date: April 2010
 #include <map>
 #include <memory> // unique_ptr
 
-#include <util/guard.h>
+#include "guard.h"
 
 #include <goto-programs/goto_model.h>
 
@@ -352,8 +352,11 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
 public:
   rw_guarded_range_set_value_sett(
     const namespacet &_ns,
-    value_setst &_value_sets):
-    rw_range_set_value_sett(_ns, _value_sets)
+    value_setst &_value_sets,
+    guard_managert &guard_manager)
+    : rw_range_set_value_sett(_ns, _value_sets),
+      guard_manager(guard_manager),
+      guard(true_exprt(), guard_manager)
   {
   }
 
@@ -370,7 +373,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
     get_modet mode,
     const exprt &expr) override
   {
-    guard = guardt(true_exprt());
+    guard = guardt(true_exprt(), guard_manager);
 
     rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
   }
@@ -384,7 +387,8 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
   }
 
 protected:
-  guardt guard = guardt(true_exprt());
+  guard_managert &guard_manager;
+  guardt guard;
 
   using rw_range_sett::get_objects_rec;
 
diff --git a/src/analyses/guard.h b/src/analyses/guard.h
new file mode 100644
index 00000000000..950a65b58bc
--- /dev/null
+++ b/src/analyses/guard.h
@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: Guard Data Structure
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Guard Data Structure
+
+#ifndef CPROVER_ANALYSES_GUARD_H
+#define CPROVER_ANALYSES_GUARD_H
+
+#ifdef BDD_GUARDS
+
+#include "guard_bdd.h"
+
+using guard_managert = bdd_exprt;
+using guardt = guard_bddt;
+
+#else
+
+#include "guard_expr.h"
+
+using guard_managert = guard_expr_managert;
+using guardt = guard_exprt;
+
+#endif // BDD_GUARDS
+
+#endif // CPROVER_ANALYSES_GUARD_H
diff --git a/src/analyses/guard_bdd.cpp b/src/analyses/guard_bdd.cpp
new file mode 100644
index 00000000000..c73ee1169c1
--- /dev/null
+++ b/src/analyses/guard_bdd.cpp
@@ -0,0 +1,94 @@
+/*******************************************************************\
+
+Module: Guard Data Structure
+
+Author: Romain Brenguier, romain.brenguier@diffblue.com
+
+\*******************************************************************/
+
+/// \file
+/// Implementation of guards using BDDs
+
+#include "guard_bdd.h"
+
+#include <algorithm>
+#include <ostream>
+#include <set>
+
+#include <solvers/bdd/bdd.h>
+#include <solvers/prop/bdd_expr.h>
+#include <util/expr_util.h>
+#include <util/invariant.h>
+#include <util/make_unique.h>
+#include <util/namespace.h>
+#include <util/simplify_utils.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+guard_bddt::guard_bddt(const exprt &e, bdd_exprt &manager)
+  : manager(manager), bdd(manager.from_expr(e))
+{
+}
+
+guard_bddt &guard_bddt::operator=(const guard_bddt &other)
+{
+  PRECONDITION(&manager == &other.manager);
+  bdd = other.bdd;
+  return *this;
+}
+
+guard_bddt &guard_bddt::operator=(guard_bddt &&other)
+{
+  PRECONDITION(&manager == &other.manager);
+  std::swap(bdd, other.bdd);
+  return *this;
+}
+
+exprt guard_bddt::guard_expr(exprt expr) const
+{
+  if(is_true())
+  {
+    // do nothing
+    return expr;
+  }
+  else
+  {
+    if(expr.is_false())
+    {
+      return boolean_negate(as_expr());
+    }
+    else
+    {
+      return implies_exprt{as_expr(), expr};
+    }
+  }
+}
+
+guard_bddt &guard_bddt::append(const guard_bddt &guard)
+{
+  bdd = bdd.bdd_and(guard.bdd);
+  return *this;
+}
+
+guard_bddt &guard_bddt::add(const exprt &expr)
+{
+  bdd = bdd.bdd_and(manager.from_expr(expr));
+  return *this;
+}
+
+guard_bddt &operator-=(guard_bddt &g1, const guard_bddt &g2)
+{
+  g1.bdd = g1.bdd.constrain(g2.bdd.bdd_or(g1.bdd));
+  return g1;
+}
+
+guard_bddt &operator|=(guard_bddt &g1, const guard_bddt &g2)
+{
+  g1.bdd = g1.bdd.bdd_or(g2.bdd);
+  return g1;
+}
+
+exprt guard_bddt::as_expr() const
+{
+  return manager.as_expr(bdd);
+}
diff --git a/src/analyses/guard_bdd.h b/src/analyses/guard_bdd.h
new file mode 100644
index 00000000000..c522b242cdd
--- /dev/null
+++ b/src/analyses/guard_bdd.h
@@ -0,0 +1,78 @@
+/*******************************************************************\
+
+Module: Guard Data Structure
+
+Author: Romain Brenguier, romain.brenguier@diffblue.com
+
+\*******************************************************************/
+
+/// \file
+/// Guard Data Structure
+/// Implementation using BDDs
+
+#ifndef CPROVER_ANALYSES_GUARD_BDD_H
+#define CPROVER_ANALYSES_GUARD_BDD_H
+
+#include <iosfwd>
+#include <memory>
+
+#include <solvers/bdd/bdd.h>
+#include <solvers/prop/bdd_expr.h>
+#include <util/make_unique.h>
+#include <util/std_expr.h>
+
+class guard_bddt
+{
+public:
+  guard_bddt(const exprt &e, bdd_exprt &manager);
+  guard_bddt(const guard_bddt &other) : manager(other.manager), bdd(other.bdd)
+  {
+  }
+
+  guard_bddt &operator=(const guard_bddt &other);
+  guard_bddt &operator=(guard_bddt &&other);
+  guard_bddt &add(const exprt &expr);
+  guard_bddt &append(const guard_bddt &guard);
+  exprt as_expr() const;
+
+  /// BDDs are always in a simplified form and thus no further simplification
+  /// is required after calls to \ref as_expr().
+  /// This can vary according to the guard implementation.
+  static constexpr bool is_always_simplified = true;
+
+  /// Return `guard => dest` or a simplified variant thereof if either guard or
+  /// dest are trivial.
+  exprt guard_expr(exprt expr) const;
+
+  bool is_true() const
+  {
+    return bdd.is_true();
+  }
+
+  bool is_false() const
+  {
+    return bdd.is_false();
+  }
+
+  /// Transforms \p g1 into \c g1' such that `g1' & g2 => g1 => g1'`
+  /// and returns a reference to g1.
+  friend guard_bddt &operator-=(guard_bddt &g1, const guard_bddt &g2);
+
+  friend guard_bddt &operator|=(guard_bddt &g1, const guard_bddt &g2);
+
+  guard_bddt operator!() const
+  {
+    return guard_bddt(manager, bdd.bdd_not());
+  }
+
+private:
+  bdd_exprt &manager;
+  bddt bdd;
+
+  guard_bddt(bdd_exprt &manager, bddt bdd)
+    : manager(manager), bdd(std::move(bdd))
+  {
+  }
+};
+
+#endif // CPROVER_ANALYSES_GUARD_BDD_H
diff --git a/src/util/guard.cpp b/src/analyses/guard_expr.cpp
similarity index 62%
rename from src/util/guard.cpp
rename to src/analyses/guard_expr.cpp
index c74245a1301..ef48e8fde13 100644
--- a/src/util/guard.cpp
+++ b/src/analyses/guard_expr.cpp
@@ -9,36 +9,36 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Symbolic Execution
 
-#include "guard.h"
+#include "guard_expr.h"
 
 #include <ostream>
 
-#include "expr_util.h"
-#include "invariant.h"
-#include "simplify_utils.h"
-#include "std_expr.h"
+#include <util/expr_util.h>
+#include <util/invariant.h>
+#include <util/simplify_utils.h>
+#include <util/std_expr.h>
 
-void guardt::guard_expr(exprt &dest) const
+exprt guard_exprt::guard_expr(exprt expr) const
 {
   if(is_true())
   {
     // do nothing
+    return expr;
   }
   else
   {
-    if(dest.is_false())
+    if(expr.is_false())
     {
-      dest = boolean_negate(as_expr());
+      return boolean_negate(as_expr());
     }
     else
     {
-      implies_exprt tmp(as_expr(), dest);
-      dest.swap(tmp);
+      return implies_exprt{as_expr(), expr};
     }
   }
 }
 
-void guardt::add(const exprt &expr)
+void guard_exprt::add(const exprt &expr)
 {
   PRECONDITION(expr.type().id() == ID_bool);
 
@@ -58,15 +58,13 @@ void guardt::add(const exprt &expr)
 
   exprt::operandst &op = this->expr.operands();
 
-  if(expr.id()==ID_and)
-    op.insert(op.end(),
-              expr.operands().begin(),
-              expr.operands().end());
+  if(expr.id() == ID_and)
+    op.insert(op.end(), expr.operands().begin(), expr.operands().end());
   else
     op.push_back(expr);
 }
 
-guardt &operator -= (guardt &g1, const guardt &g2)
+guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2)
 {
   if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
     return g1;
@@ -76,18 +74,16 @@ guardt &operator -= (guardt &g1, const guardt &g2)
   sort_and_join(g2_sorted);
 
   exprt::operandst &op1 = g1.expr.operands();
-  const exprt::operandst &op2=g2_sorted.operands();
+  const exprt::operandst &op2 = g2_sorted.operands();
 
-  exprt::operandst::iterator it1=op1.begin();
-  for(exprt::operandst::const_iterator
-      it2=op2.begin();
-      it2!=op2.end();
+  exprt::operandst::iterator it1 = op1.begin();
+  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
       ++it2)
   {
-    while(it1!=op1.end() && *it1<*it2)
+    while(it1 != op1.end() && *it1 < *it2)
       ++it1;
-    if(it1!=op1.end() && *it1==*it2)
-      it1=op1.erase(it1);
+    if(it1 != op1.end() && *it1 == *it2)
+      it1 = op1.erase(it1);
   }
 
   g1.expr = conjunction(op1);
@@ -95,7 +91,7 @@ guardt &operator -= (guardt &g1, const guardt &g2)
   return g1;
 }
 
-guardt &operator |= (guardt &g1, const guardt &g2)
+guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2)
 {
   if(g2.is_false() || g1.is_true())
     return g1;
@@ -125,46 +121,44 @@ guardt &operator |= (guardt &g1, const guardt &g2)
   sort_and_join(g2_sorted);
 
   exprt::operandst &op1 = g1.expr.operands();
-  const exprt::operandst &op2=g2_sorted.operands();
+  const exprt::operandst &op2 = g2_sorted.operands();
 
   exprt::operandst n_op1, n_op2;
   n_op1.reserve(op1.size());
   n_op2.reserve(op2.size());
 
-  exprt::operandst::iterator it1=op1.begin();
-  for(exprt::operandst::const_iterator
-      it2=op2.begin();
-      it2!=op2.end();
+  exprt::operandst::iterator it1 = op1.begin();
+  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
       ++it2)
   {
-    while(it1!=op1.end() && *it1<*it2)
+    while(it1 != op1.end() && *it1 < *it2)
     {
       n_op1.push_back(*it1);
-      it1=op1.erase(it1);
+      it1 = op1.erase(it1);
     }
-    if(it1!=op1.end() && *it1==*it2)
+    if(it1 != op1.end() && *it1 == *it2)
       ++it1;
     else
       n_op2.push_back(*it2);
   }
-  while(it1!=op1.end())
+  while(it1 != op1.end())
   {
     n_op1.push_back(*it1);
-    it1=op1.erase(it1);
+    it1 = op1.erase(it1);
   }
 
   if(n_op2.empty())
     return g1;
 
   // end of common prefix
-  exprt and_expr1=conjunction(n_op1);
-  exprt and_expr2=conjunction(n_op2);
+  exprt and_expr1 = conjunction(n_op1);
+  exprt and_expr2 = conjunction(n_op2);
 
   g1.expr = conjunction(op1);
 
   exprt tmp(boolean_negate(and_expr2));
 
-  if(tmp!=and_expr1)
+  if(tmp != and_expr1)
   {
     if(and_expr1.is_true() || and_expr2.is_true())
     {
diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h
new file mode 100644
index 00000000000..774659821cf
--- /dev/null
+++ b/src/analyses/guard_expr.h
@@ -0,0 +1,79 @@
+/*******************************************************************\
+
+Module: Guard Data Structure
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Guard Data Structure
+
+#ifndef CPROVER_ANALYSES_GUARD_EXPR_H
+#define CPROVER_ANALYSES_GUARD_EXPR_H
+
+#include <iosfwd>
+
+#include <util/std_expr.h>
+
+/// This is unused by this implementation of guards, but can be used by other
+/// implementations of the same interface.
+struct guard_expr_managert
+{
+};
+
+class guard_exprt
+{
+public:
+  /// Construct a BDD from an expression
+  /// The \c guard_managert parameter is not used, but we keep it for uniformity
+  /// with other implementations of guards which may use it.
+  explicit guard_exprt(const exprt &e, guard_expr_managert &) : expr(e)
+  {
+  }
+
+  guard_exprt &operator=(const guard_exprt &other)
+  {
+    expr = other.expr;
+    return *this;
+  }
+
+  void add(const exprt &expr);
+
+  void append(const guard_exprt &guard)
+  {
+    add(guard.as_expr());
+  }
+
+  exprt as_expr() const
+  {
+    return expr;
+  }
+
+  /// The result of \ref as_expr is not always in a simplified form
+  /// and may requires some simplification.
+  /// This can vary according to the guard implementation.
+  static constexpr bool is_always_simplified = false;
+
+  /// Return `guard => dest` or a simplified variant thereof if either guard or
+  /// dest are trivial.
+  exprt guard_expr(exprt expr) const;
+
+  bool is_true() const
+  {
+    return expr.is_true();
+  }
+
+  bool is_false() const
+  {
+    return expr.is_false();
+  }
+
+  friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);
+  friend guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2);
+
+private:
+  exprt expr;
+};
+
+#endif // CPROVER_ANALYSES_GUARD_EXPR_H
diff --git a/src/analyses/module_dependencies.txt b/src/analyses/module_dependencies.txt
index 25dc8fec88e..d3eaee11766 100644
--- a/src/analyses/module_dependencies.txt
+++ b/src/analyses/module_dependencies.txt
@@ -2,4 +2,6 @@ analyses
 goto-programs
 langapi # should go away
 pointer-analysis
+solvers/bdd
+solvers/prop
 util
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 3b1989bd2cc..44caf9e5280 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -257,6 +257,7 @@ int bmct::do_language_agnostic_bmc(
   namespacet ns(symbol_table);
   messaget message(ui);
   std::unique_ptr<path_storaget> worklist;
+  guard_managert guard_manager;
   std::string strategy = opts.get_option("exploration-strategy");
   worklist = get_path_strategy(strategy);
   try
@@ -268,7 +269,14 @@ 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, *worklist, callback_after_symex);
+      bmct bmc(
+        opts,
+        symbol_table,
+        ui,
+        pc,
+        *worklist,
+        callback_after_symex,
+        guard_manager);
       if(driver_configure_bmc)
         driver_configure_bmc(bmc, symbol_table);
       tmp_result = bmc.run(model);
@@ -319,6 +327,7 @@ int bmct::do_language_agnostic_bmc(
         resume.equation,
         resume.state,
         *worklist,
+        guard_manager,
         callback_after_symex);
       if(driver_configure_bmc)
         driver_configure_bmc(pe, symbol_table);
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 9c879e1ecca..b5bc58a6421 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -70,19 +70,22 @@ class bmct:public safety_checkert
     ui_message_handlert &_message_handler,
     prop_convt &_prop_conv,
     path_storaget &_path_storage,
-    std::function<bool(void)> callback_after_symex)
+    std::function<bool(void)> callback_after_symex,
+    guard_managert &guard_manager)
     : safety_checkert(ns, _message_handler),
       options(_options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table, symex_symbol_table),
       equation(_message_handler),
+      guard_manager(guard_manager),
       path_storage(_path_storage),
       symex(
         _message_handler,
         outer_symbol_table,
         equation,
         options,
-        path_storage),
+        path_storage,
+        guard_manager),
       prop_conv(_prop_conv),
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
@@ -140,19 +143,22 @@ class bmct:public safety_checkert
     prop_convt &_prop_conv,
     symex_target_equationt &_equation,
     path_storaget &_path_storage,
-    std::function<bool(void)> callback_after_symex)
+    std::function<bool(void)> callback_after_symex,
+    guard_managert &guard_manager)
     : safety_checkert(ns, _message_handler),
       options(_options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       equation(_equation),
+      guard_manager(guard_manager),
       path_storage(_path_storage),
       symex(
         _message_handler,
         outer_symbol_table,
         equation,
         options,
-        path_storage),
+        path_storage,
+        guard_manager),
       prop_conv(_prop_conv),
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
@@ -170,6 +176,7 @@ class bmct:public safety_checkert
   symbol_tablet symex_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
+  guard_managert &guard_manager;
   path_storaget &path_storage;
   symex_bmct symex;
   prop_convt &prop_conv;
@@ -231,6 +238,7 @@ class path_explorert : public bmct
     symex_target_equationt &saved_equation,
     const goto_symex_statet &saved_state,
     path_storaget &path_storage,
+    guard_managert &guard_manager,
     std::function<bool(void)> callback_after_symex)
     : bmct(
         _options,
@@ -239,7 +247,8 @@ class path_explorert : public bmct
         _prop_conv,
         saved_equation,
         path_storage,
-        callback_after_symex),
+        callback_after_symex,
+        guard_manager),
       saved_state(saved_state)
   {
   }
diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp
index c4e0cca89e4..5fdacdeec2f 100644
--- a/src/goto-checker/multi_path_symex_only_checker.cpp
+++ b/src/goto-checker/multi_path_symex_only_checker.cpp
@@ -32,7 +32,8 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
       goto_model.get_symbol_table(),
       equation,
       options,
-      path_storage)
+      path_storage,
+      guard_manager)
 {
   setup_symex(symex, ns, options, ui_message_handler);
 }
diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h
index 2d8a72ab0f1..851a2eb7827 100644
--- a/src/goto-checker/multi_path_symex_only_checker.h
+++ b/src/goto-checker/multi_path_symex_only_checker.h
@@ -31,6 +31,7 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert
   symbol_tablet symex_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
+  guard_managert guard_manager;
   path_fifot path_storage; // should go away
   symex_bmct symex;
 };
diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp
index 4428346e29d..5fb86458a62 100644
--- a/src/goto-checker/single_path_symex_checker.cpp
+++ b/src/goto-checker/single_path_symex_checker.cpp
@@ -55,7 +55,8 @@ operator()(propertiest &properties)
       goto_model.get_symbol_table(),
       equation,
       options,
-      *worklist);
+      *worklist,
+      guard_manager);
     setup_symex(symex);
 
     symex.initialize_path_storage_from_entry_point_of(
@@ -70,7 +71,8 @@ operator()(propertiest &properties)
       goto_model.get_symbol_table(),
       resume.equation,
       options,
-      *worklist);
+      *worklist,
+      guard_manager);
     setup_symex(symex);
 
     symex.resume_symex_from_saved_state(
diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp
index 81d95e59b67..0bf7938ac13 100644
--- a/src/goto-checker/single_path_symex_only_checker.cpp
+++ b/src/goto-checker/single_path_symex_only_checker.cpp
@@ -45,7 +45,8 @@ operator()(propertiest &properties)
       goto_model.get_symbol_table(),
       equation,
       options,
-      *worklist);
+      *worklist,
+      guard_manager);
     setup_symex(symex);
 
     symex.initialize_path_storage_from_entry_point_of(
@@ -60,7 +61,8 @@ operator()(propertiest &properties)
       goto_model.get_symbol_table(),
       resume.equation,
       options,
-      *worklist);
+      *worklist,
+      guard_manager);
     setup_symex(symex);
 
     symex.resume_symex_from_saved_state(
diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h
index 008c882bcf0..77ca35623ce 100644
--- a/src/goto-checker/single_path_symex_only_checker.h
+++ b/src/goto-checker/single_path_symex_only_checker.h
@@ -35,6 +35,7 @@ class single_path_symex_only_checkert : public incremental_goto_checkert
   abstract_goto_modelt &goto_model;
   symbol_tablet symex_symbol_table;
   namespacet ns;
+  guard_managert guard_manager;
   std::unique_ptr<path_storaget> worklist;
 
   void equation_output(
diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
index 7252e23e69b..61cf628c18b 100644
--- a/src/goto-checker/symex_bmc.cpp
+++ b/src/goto-checker/symex_bmc.cpp
@@ -23,8 +23,15 @@ symex_bmct::symex_bmct(
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &_target,
   const optionst &options,
-  path_storaget &path_storage)
-  : goto_symext(mh, outer_symbol_table, _target, options, path_storage),
+  path_storaget &path_storage,
+  guard_managert &guard_manager)
+  : goto_symext(
+      mh,
+      outer_symbol_table,
+      _target,
+      options,
+      path_storage,
+      guard_manager),
     record_coverage(!options.get_option("symex-coverage-report").empty()),
     symex_coverage(ns)
 {
diff --git a/src/goto-checker/symex_bmc.h b/src/goto-checker/symex_bmc.h
index 5e322d53090..2f9bc6b16b6 100644
--- a/src/goto-checker/symex_bmc.h
+++ b/src/goto-checker/symex_bmc.h
@@ -30,7 +30,8 @@ class symex_bmct : public goto_symext
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
     const optionst &options,
-    path_storaget &path_storage);
+    path_storaget &path_storage,
+    guard_managert &guard_manager);
 
   // To show progress
   source_locationt last_source_location;
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 55d87def22b..f37a8afe8fd 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -115,7 +115,8 @@ int acceleratet::accelerate_loop(goto_programt::targett &loop_header)
     program,
     loop,
     loop_header,
-    accelerate_limit);
+    accelerate_limit,
+    guard_manager);
 #else
   disjunctive_polynomial_accelerationt
     acceleration(symbol_table, goto_functions, program, loop, loop_header);
@@ -335,7 +336,7 @@ void acceleratet::set_dirty_vars(path_acceleratort &accelerator)
 
     if(jt==dirty_vars_map.end())
     {
-      scratch_programt scratch(symbol_table, message_handler);
+      scratch_programt scratch(symbol_table, message_handler, guard_manager);
       symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());
       dirty_var=new_sym.symbol_expr();
       dirty_vars_map[*it]=dirty_var;
@@ -512,7 +513,8 @@ void acceleratet::insert_automaton(trace_automatont &automaton)
   // machine.
   for(const auto &sym : automaton.alphabet)
   {
-    scratch_programt state_machine(symbol_table, message_handler);
+    scratch_programt state_machine{
+      symbol_table, message_handler, guard_manager};
     trace_automatont::sym_range_pairt p=transitions.equal_range(sym);
 
     build_state_machine(p.first, p.second, accept_states, state, next_state,
@@ -651,13 +653,14 @@ int acceleratet::accelerate_loops()
 void accelerate_functions(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  bool use_z3)
+  bool use_z3,
+  guard_managert &guard_manager)
 {
   Forall_goto_functions(it, goto_model.goto_functions)
   {
     std::cout << "Accelerating function " << it->first << '\n';
     acceleratet accelerate(
-      it->second.body, goto_model, message_handler, use_z3);
+      it->second.body, goto_model, message_handler, use_z3, guard_manager);
 
     int num_accelerated=accelerate.accelerate_loops();
 
diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h
index 9535852041b..c8e2b0f4c9c 100644
--- a/src/goto-instrument/accelerate/accelerate.h
+++ b/src/goto-instrument/accelerate/accelerate.h
@@ -34,11 +34,13 @@ class acceleratet
     goto_programt &_program,
     goto_modelt &_goto_model,
     message_handlert &message_handler,
-    bool _use_z3)
+    bool _use_z3,
+    guard_managert &guard_manager)
     : message_handler(message_handler),
       program(_program),
       goto_functions(_goto_model.goto_functions),
       symbol_table(_goto_model.symbol_table),
+      guard_manager(guard_manager),
       ns(_goto_model.symbol_table),
       utils(symbol_table, message_handler, goto_functions),
       use_z3(_use_z3)
@@ -113,6 +115,7 @@ class acceleratet
   goto_programt &program;
   goto_functionst &goto_functions;
   symbol_tablet &symbol_table;
+  guard_managert &guard_manager;
   namespacet ns;
   natural_loops_mutablet natural_loops;
   subsumed_pathst subsumed;
@@ -130,6 +133,7 @@ class acceleratet
 void accelerate_functions(
   goto_modelt &,
   message_handlert &message_handler,
-  bool use_z3);
+  bool use_z3,
+  guard_managert &guard_manager);
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index d64246c8f0b..95c3e1da5a4 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -110,10 +110,10 @@ void acceleration_utilst::find_modified(
   }
 }
 
-
 bool acceleration_utilst::check_inductive(
   std::map<exprt, polynomialt> polynomials,
-  patht &path)
+  patht &path,
+  guard_managert &guard_manager)
 {
   // Checking that our polynomial is inductive with respect to the loop body is
   // equivalent to checking safety of the following program:
@@ -126,7 +126,7 @@ bool acceleration_utilst::check_inductive(
   // assert (target1==polynomial1);
   // assert (target2==polynomial2);
   // ...
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program(symbol_table, message_handler, guard_manager);
   std::vector<exprt> polynomials_hold;
   substitutiont substitution;
 
@@ -162,7 +162,7 @@ bool acceleration_utilst::check_inductive(
 
   try
   {
-    if(program.check_sat())
+    if(program.check_sat(guard_manager))
     {
       // We found a counterexample to inductiveness... :-(
   #ifdef DEBUG
@@ -353,7 +353,8 @@ void acceleration_utilst::push_nondet(exprt &expr)
 bool acceleration_utilst::do_assumptions(
   std::map<exprt, polynomialt> polynomials,
   patht &path,
-  exprt &guard)
+  exprt &guard,
+  guard_managert &guard_manager)
 {
   // We want to check that if an assumption fails, the next iteration can't be
   // feasible again.  To do this we check the following program for safety:
@@ -380,7 +381,7 @@ bool acceleration_utilst::do_assumptions(
   // assert(!precondition);
 
   exprt condition=precondition(path);
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program(symbol_table, message_handler, guard_manager);
 
   substitutiont substitution;
   stash_polynomials(program, polynomials, substitution, path);
@@ -445,7 +446,7 @@ bool acceleration_utilst::do_assumptions(
 
   try
   {
-    if(program.check_sat())
+    if(program.check_sat(guard_manager))
     {
   #ifdef DEBUG
       std::cout << "Path is not monotone\n";
diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h
index c9213919376..d62f4e6eb3a 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.h
+++ b/src/goto-instrument/accelerate/acceleration_utils.h
@@ -64,12 +64,15 @@ class acceleration_utilst
   {
   }
 
-  void extract_polynomial(scratch_programt &program,
-                          std::set<std::pair<expr_listt, exprt> > &coefficients,
-                          polynomialt &polynomial);
-
-  bool check_inductive(std::map<exprt, polynomialt> polynomials,
-                       patht &path);
+  void extract_polynomial(
+    scratch_programt &program,
+    std::set<std::pair<expr_listt, exprt>> &coefficients,
+    polynomialt &polynomial);
+
+  bool check_inductive(
+    std::map<exprt, polynomialt> polynomials,
+    patht &path,
+    guard_managert &guard_manager);
   void stash_variables(scratch_programt &program,
                        expr_sett modified,
                        substitutiont &substitution);
@@ -82,9 +85,11 @@ class acceleration_utilst
   void abstract_arrays(exprt &expr, expr_mapt &abstractions);
   void push_nondet(exprt &expr);
 
-  bool do_assumptions(std::map<exprt, polynomialt> polynomials,
-                      patht &body,
-                      exprt &guard);
+  bool do_assumptions(
+    std::map<exprt, polynomialt> polynomials,
+    patht &body,
+    exprt &guard,
+    guard_managert &guard_manager);
 
   typedef std::pair<exprt, exprt> expr_pairt;
   typedef std::vector<expr_pairt> expr_pairst;
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index de17d162fce..c2a75aaf40f 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -50,7 +50,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   path_acceleratort &accelerator)
 {
   std::map<exprt, polynomialt> polynomials;
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program{symbol_table, message_handler, guard_manager};
 
   accelerator.clear();
 
@@ -143,7 +143,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   expr_sett dirty;
   utils.find_modified(accelerator.path, dirty);
   polynomial_acceleratort path_acceleration(
-    message_handler, symbol_table, goto_functions, loop_counter);
+    message_handler, symbol_table, goto_functions, loop_counter, guard_manager);
   goto_programt::instructionst assigns;
 
   for(patht::iterator it=accelerator.path.begin();
@@ -212,7 +212,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
       std::map<exprt, polynomialt> this_poly;
       this_poly[target]=poly;
 
-      if(utils.check_inductive(this_poly, accelerator.path))
+      if(utils.check_inductive(this_poly, accelerator.path, guard_manager))
       {
         polynomials[target]=poly;
         accelerator.changed_vars.insert(target);
@@ -245,7 +245,8 @@ bool disjunctive_polynomial_accelerationt::accelerate(
 
   try
   {
-    path_is_monotone=utils.do_assumptions(polynomials, path, guard);
+    path_is_monotone =
+      utils.do_assumptions(polynomials, path, guard, guard_manager);
   }
   catch(const std::string &s)
   {
@@ -337,7 +338,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
 
 bool disjunctive_polynomial_accelerationt::find_path(patht &path)
 {
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program{symbol_table, message_handler, guard_manager};
 
   program.append(fixed);
   program.append(fixed);
@@ -373,7 +374,7 @@ bool disjunctive_polynomial_accelerationt::find_path(patht &path)
 
   try
   {
-    if(program.check_sat())
+    if(program.check_sat(guard_manager))
     {
 #ifdef DEBUG
       std::cout << "Found a path\n";
@@ -405,7 +406,7 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial(
   std::vector<expr_listt> parameters;
   std::set<std::pair<expr_listt, exprt> > coefficients;
   expr_listt exprs;
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program{symbol_table, message_handler, guard_manager};
   expr_sett influence;
 
   cone_of_influence(var, influence);
@@ -619,7 +620,7 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial(
   // relevant coefficients and return the expression.
   try
   {
-    if(program.check_sat())
+    if(program.check_sat(guard_manager))
     {
 #ifdef DEBUG
       std::cout << "Found a polynomial\n";
@@ -855,7 +856,7 @@ void disjunctive_polynomial_accelerationt::build_path(
  */
 void disjunctive_polynomial_accelerationt::build_fixed()
 {
-  scratch_programt scratch(symbol_table, message_handler);
+  scratch_programt scratch{symbol_table, message_handler, guard_manager};
   std::map<exprt, exprt> shadow_distinguishers;
 
   fixed.copy_from(goto_program);
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h
index 9fef71f077b..ba11ca64d2a 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h
@@ -39,12 +39,14 @@ class disjunctive_polynomial_accelerationt
     goto_functionst &_goto_functions,
     goto_programt &_goto_program,
     natural_loops_mutablet::natural_loopt &_loop,
-    goto_programt::targett _loop_header)
+    goto_programt::targett _loop_header,
+    guard_managert &guard_manager)
     : message_handler(message_handler),
       symbol_table(_symbol_table),
       ns(symbol_table),
       goto_functions(_goto_functions),
       goto_program(_goto_program),
+      guard_manager(guard_manager),
       loop(_loop),
       loop_header(_loop_header),
       utils(symbol_table, message_handler, goto_functions, loop_counter)
@@ -89,6 +91,7 @@ class disjunctive_polynomial_accelerationt
   namespacet ns;
   goto_functionst &goto_functions;
   goto_programt &goto_program;
+  guard_managert &guard_manager;
   natural_loops_mutablet::natural_loopt &loop;
   goto_programt::targett loop_header;
 
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
index df014cb11f2..ced470f3bd5 100644
--- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
+++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
@@ -36,22 +36,28 @@ class enumerating_loop_accelerationt
     goto_programt &_goto_program,
     natural_loops_mutablet::natural_loopt &_loop,
     goto_programt::targett _loop_header,
-    int _path_limit)
+    int _path_limit,
+    guard_managert &guard_manager)
     : symbol_table(_symbol_table),
       goto_functions(_goto_functions),
       goto_program(_goto_program),
       loop(_loop),
       loop_header(_loop_header),
-      polynomial_accelerator(message_handler, symbol_table, goto_functions),
+      guard_manager(guard_manager),
+      polynomial_accelerator(
+        message_handler,
+        symbol_table,
+        goto_functions,
+        guard_manager),
       path_limit(_path_limit),
-      path_enumerator(
-        util_make_unique<sat_path_enumeratort>(
-          message_handler,
-          symbol_table,
-          goto_functions,
-          goto_program,
-          loop,
-          loop_header))
+      path_enumerator(util_make_unique<sat_path_enumeratort>(
+        message_handler,
+        symbol_table,
+        goto_functions,
+        goto_program,
+        loop,
+        loop_header,
+        guard_manager))
   {
   }
 
@@ -63,6 +69,7 @@ class enumerating_loop_accelerationt
   goto_programt &goto_program;
   natural_loops_mutablet::natural_loopt &loop;
   goto_programt::targett loop_header;
+  guard_managert &guard_manager;
   polynomial_acceleratort polynomial_accelerator;
   int path_limit;
 
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 746596aa469..4989b494584 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -58,7 +58,7 @@ bool polynomial_acceleratort::accelerate(
 
   expr_sett targets;
   std::map<exprt, polynomialt> polynomials;
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program{symbol_table, message_handler, guard_manager};
   goto_programt::instructionst assigns;
 
   utils.find_modified(body, targets);
@@ -178,7 +178,8 @@ bool polynomial_acceleratort::accelerate(
 
   try
   {
-    path_is_monotone=utils.do_assumptions(polynomials, loop, guard);
+    path_is_monotone =
+      utils.do_assumptions(polynomials, loop, guard, guard_manager);
   }
   catch(const std::string &s)
   {
@@ -284,7 +285,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
   std::vector<expr_listt> parameters;
   std::set<std::pair<expr_listt, exprt> > coefficients;
   expr_listt exprs;
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program{symbol_table, message_handler, guard_manager};
   exprt overflow_var =
     utils.fresh_symbol("polynomial::overflow", bool_typet()).symbol_expr();
   overflow_instrumentert overflow(program, overflow_var, symbol_table);
@@ -412,7 +413,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
   // relevant coefficients and return the expression.
   try
   {
-    if(program.check_sat())
+    if(program.check_sat(guard_manager))
     {
       utils.extract_polynomial(program, coefficients, polynomial);
       return true;
@@ -666,7 +667,7 @@ bool polynomial_acceleratort::check_inductive(
   // assert (target1==polynomial1);
   // assert (target2==polynomial2);
   // ...
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program{symbol_table, message_handler, guard_manager};
   std::vector<exprt> polynomials_hold;
   substitutiont substitution;
 
@@ -703,7 +704,7 @@ bool polynomial_acceleratort::check_inductive(
 
   try
   {
-    if(program.check_sat())
+    if(program.check_sat(guard_manager))
     {
       // We found a counterexample to inductiveness... :-(
   #ifdef DEBUG
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-instrument/accelerate/polynomial_accelerator.h
index a9d2eb8ff40..a05c16ecdd0 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.h
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.h
@@ -34,11 +34,13 @@ class polynomial_acceleratort
   polynomial_acceleratort(
     message_handlert &message_handler,
     const symbol_tablet &_symbol_table,
-    const goto_functionst &_goto_functions)
+    const goto_functionst &_goto_functions,
+    guard_managert &guard_manager)
     : message_handler(message_handler),
       symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
       ns(symbol_table),
       goto_functions(_goto_functions),
+      guard_manager(guard_manager),
       utils(symbol_table, message_handler, goto_functions, loop_counter)
   {
     loop_counter=nil_exprt();
@@ -48,11 +50,13 @@ class polynomial_acceleratort
     message_handlert &message_handler,
     const symbol_tablet &_symbol_table,
     const goto_functionst &_goto_functions,
-    exprt &_loop_counter)
+    exprt &_loop_counter,
+    guard_managert &guard_manager)
     : message_handler(message_handler),
       symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
       ns(symbol_table),
       goto_functions(_goto_functions),
+      guard_manager(guard_manager),
       utils(symbol_table, message_handler, goto_functions, loop_counter),
       loop_counter(_loop_counter)
   {
@@ -153,6 +157,7 @@ class polynomial_acceleratort
   symbol_tablet &symbol_table;
   const namespacet ns;
   const goto_functionst &goto_functions;
+  guard_managert &guard_manager;
   acceleration_utilst utils;
 
   exprt loop_counter;
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index 3dd2bb2ab36..56ba3bda277 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -47,7 +47,7 @@ Author: Matt Lewis
 
 bool sat_path_enumeratort::next(patht &path)
 {
-  scratch_programt program(symbol_table, message_handler);
+  scratch_programt program{symbol_table, message_handler, guard_manager};
 
   program.append(fixed);
   program.append(fixed);
@@ -83,7 +83,7 @@ bool sat_path_enumeratort::next(patht &path)
 
   try
   {
-    if(program.check_sat())
+    if(program.check_sat(guard_manager))
     {
 #ifdef DEBUG
       std::cout << "Found a path\n";
@@ -212,7 +212,7 @@ void sat_path_enumeratort::build_path(
  */
 void sat_path_enumeratort::build_fixed()
 {
-  scratch_programt scratch(symbol_table, message_handler);
+  scratch_programt scratch{symbol_table, message_handler, guard_manager};
   std::map<exprt, exprt> shadow_distinguishers;
 
   fixed.copy_from(goto_program);
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.h b/src/goto-instrument/accelerate/sat_path_enumerator.h
index 155785e6994..c2b055e67a1 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.h
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.h
@@ -39,7 +39,8 @@ class sat_path_enumeratort:public path_enumeratort
     goto_functionst &_goto_functions,
     goto_programt &_goto_program,
     natural_loops_mutablet::natural_loopt &_loop,
-    goto_programt::targett _loop_header)
+    goto_programt::targett _loop_header,
+    guard_managert &guard_manager)
     : message_handler(message_handler),
       symbol_table(_symbol_table),
       ns(symbol_table),
@@ -47,7 +48,8 @@ class sat_path_enumeratort:public path_enumeratort
       goto_program(_goto_program),
       loop(_loop),
       loop_header(_loop_header),
-      utils(symbol_table, message_handler, goto_functions, loop_counter)
+      utils(symbol_table, message_handler, goto_functions, loop_counter),
+      guard_manager(guard_manager)
   {
     find_distinguishing_points();
     build_fixed();
@@ -75,6 +77,7 @@ class sat_path_enumeratort:public path_enumeratort
   typedef std::map<exprt, bool> distinguish_valuest;
 
   acceleration_utilst utils;
+  guard_managert &guard_manager;
   exprt loop_counter;
   distinguish_mapt distinguishing_points;
   std::list<exprt> distinguishers;
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index 78349142762..de101357478 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -22,7 +22,7 @@ Author: Matt Lewis
 #include <iostream>
 #endif
 
-bool scratch_programt::check_sat(bool do_slice)
+bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
 {
   fix_types();
 
@@ -36,7 +36,8 @@ bool scratch_programt::check_sat(bool do_slice)
 #endif
 
   symex_state = util_make_unique<goto_symex_statet>(
-    symex_targett::sourcet(goto_functionst::entry_point(), *this));
+    symex_targett::sourcet(goto_functionst::entry_point(), *this),
+    guard_manager);
   symex.symex_with_state(
     *symex_state,
     [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
index a0f294bae4f..a5b65df78a6 100644
--- a/src/goto-instrument/accelerate/scratch_program.h
+++ b/src/goto-instrument/accelerate/scratch_program.h
@@ -36,7 +36,10 @@ Author: Matt Lewis
 class scratch_programt:public goto_programt
 {
 public:
-  scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh)
+  scratch_programt(
+    symbol_tablet &_symbol_table,
+    message_handlert &mh,
+    guard_managert &guard_manager)
     : constant_propagation(true),
       symbol_table(_symbol_table),
       symex_symbol_table(),
@@ -44,7 +47,7 @@ class scratch_programt:public goto_programt
       equation(mh),
       path_storage(),
       options(get_default_options()),
-      symex(mh, symbol_table, equation, options, path_storage),
+      symex(mh, symbol_table, equation, options, path_storage, guard_manager),
       satcheck(util_make_unique<satcheckt>(mh)),
       satchecker(ns, *satcheck),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
@@ -60,11 +63,11 @@ class scratch_programt:public goto_programt
   targett assign(const exprt &lhs, const exprt &rhs);
   targett assume(const exprt &guard);
 
-  bool check_sat(bool do_slice);
+  bool check_sat(bool do_slice, guard_managert &guard_manager);
 
-  bool check_sat()
+  bool check_sat(guard_managert &guard_manager)
   {
-    return check_sat(true);
+    return check_sat(true, guard_manager);
   }
 
   exprt eval(const exprt &e);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 1b868cdce13..3772246accd 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -764,8 +764,9 @@ int goto_instrument_parse_optionst::doit()
       remove_calls_no_body(goto_model.goto_functions);
 
       status() << "Accelerating" << eom;
+      guard_managert guard_manager;
       accelerate_functions(
-        goto_model, get_message_handler(), cmdline.isset("z3"));
+        goto_model, get_message_handler(), cmdline.isset("z3"), guard_manager);
       remove_skip(goto_model);
     }
 
diff --git a/src/goto-symex/CMakeLists.txt b/src/goto-symex/CMakeLists.txt
index bc2cfd0368a..303a48feb99 100644
--- a/src/goto-symex/CMakeLists.txt
+++ b/src/goto-symex/CMakeLists.txt
@@ -3,4 +3,8 @@ add_library(goto-symex ${sources})
 
 generic_includes(goto-symex)
 
+if(CMAKE_USE_CUDD)
+    target_include_directories(goto-symex PUBLIC ${CUDD_INCLUDE}/cudd/)
+endif()
+
 target_link_libraries(goto-symex util)
diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h
index c34c7df98da..10f7fb64a21 100644
--- a/src/goto-symex/goto_state.h
+++ b/src/goto-symex/goto_state.h
@@ -12,9 +12,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
 #define CPROVER_GOTO_SYMEX_GOTO_STATE_H
 
+#include <analyses/guard.h>
 #include <analyses/local_safe_pointers.h>
 #include <pointer-analysis/value_set.h>
-#include <util/guard.h>
 
 #include "renaming_level.h"
 #include "symex_target_equation.h"
@@ -39,7 +39,7 @@ class goto_statet
   // the if branch will be guarded by the condition of the if (and if there
   // is an else branch then instructions on it will be guarded by the negation
   // of the condition of the if).
-  guardt guard{true_exprt{}};
+  guardt guard;
 
   symex_targett::sourcet source;
 
@@ -62,7 +62,11 @@ class goto_statet
 
   /// Constructors
   explicit goto_statet(const class goto_symex_statet &s);
-  explicit goto_statet(const symex_targett::sourcet &_source) : source(_source)
+
+  goto_statet(
+    const symex_targett::sourcet &_source,
+    guard_managert &guard_manager)
+    : guard(true_exprt(), guard_manager), source(_source)
   {
   }
 };
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index a4c68471a7f..72e6a8581e7 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -27,7 +27,6 @@ class code_assignt;
 class code_function_callt;
 class exprt;
 class goto_symex_statet;
-class guardt;
 class if_exprt;
 class index_exprt;
 class symbol_exprt;
@@ -89,16 +88,19 @@ class goto_symext
   /// \param options: The options to use to configure this execution
   /// \param path_storage: Place to storage symbolic execution paths that have
   /// been halted and can be resumed later
+  /// \param guard_manager: Manager for creating guards
   goto_symext(
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
     const optionst &options,
-    path_storaget &path_storage)
+    path_storaget &path_storage,
+    guard_managert &guard_manager)
     : should_pause_symex(false),
       symex_config(options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
+      guard_manager(guard_manager),
       target(_target),
       atomic_section_counter(0),
       log(mh),
@@ -245,6 +247,11 @@ class goto_symext
   /// goto-program, and the names of dynamically-created objects.
   namespacet ns;
 
+  /// Used to create guards. Guards created with different guard managers cannot
+  /// be combined together, so guards created by goto-symex should not escape
+  /// the scope of this manager.
+  guard_managert &guard_manager;
+
   /// The equation that this execution is building up
   symex_target_equationt &target;
 
@@ -445,49 +452,49 @@ class goto_symext
     const exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    guardt &,
+    exprt::operandst &,
     assignment_typet);
   void symex_assign_symbol(
     statet &,
     const ssa_exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    guardt &,
+    exprt::operandst &,
     assignment_typet);
   void symex_assign_typecast(
     statet &,
     const typecast_exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    guardt &,
+    exprt::operandst &,
     assignment_typet);
   void symex_assign_array(
     statet &,
     const index_exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    guardt &,
+    exprt::operandst &,
     assignment_typet);
   void symex_assign_struct_member(
     statet &,
     const member_exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    guardt &,
+    exprt::operandst &,
     assignment_typet);
   void symex_assign_if(
     statet &,
     const if_exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    guardt &,
+    exprt::operandst &,
     assignment_typet);
   void symex_assign_byte_extract(
     statet &,
     const byte_extract_exprt &lhs,
     const exprt &full_lhs,
     const exprt &rhs,
-    guardt &,
+    exprt::operandst &,
     assignment_typet);
 
   /// Store the \p what expression by recursively descending into the operands
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 6e9283025be..584a077cc20 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -29,10 +29,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 static void get_l1_name(exprt &expr);
 
-goto_symex_statet::goto_symex_statet(const symex_targett::sourcet &_source)
-  : goto_statet(_source), symex_target(nullptr), record_events(true), dirty()
+goto_symex_statet::goto_symex_statet(
+  const symex_targett::sourcet &_source,
+  guard_managert &manager)
+  : goto_statet(_source, manager),
+    guard_manager(manager),
+    symex_target(nullptr),
+    record_events(true),
+    dirty()
 {
-  threads.resize(1);
+  threads.emplace_back(guard_manager);
   call_stack().new_frame(source);
 }
 
@@ -385,7 +391,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // see whether we are within an atomic section
   if(atomic_section_id!=0)
   {
-    guardt write_guard{false_exprt{}};
+    guardt write_guard{false_exprt{}, guard_manager};
 
     const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
     if(a_s_writes!=written_in_atomic_section.end())
@@ -409,7 +415,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     // we cannot determine for sure that there has been a write already
     // so generate a read even if l1_identifier has been written on
     // all branches flowing into this read
-    guardt read_guard{false_exprt{}};
+    guardt read_guard{false_exprt{}, guard_manager};
 
     a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1];
     for(const auto &a_s_read_guard : a_s_read.second)
@@ -427,7 +433,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
 
     guardt cond = read_guard;
     if(!no_write.op().is_false())
-      cond |= guardt{no_write.op()};
+      cond |= guardt{no_write.op(), guard_manager};
 
     const renamedt<ssa_exprt, L2> l2_true_case = set_indices<L2>(ssa_l1, ns);
 
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 88a0c8549a3..9b42c09417b 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_set>
 
 #include <analyses/dirty.h>
+#include <analyses/guard.h>
 
 #include <util/invariant.h>
-#include <util/guard.h>
 #include <util/std_expr.h>
 #include <util/ssa_expr.h>
 #include <util/make_unique.h>
@@ -41,7 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class goto_symex_statet final : public goto_statet
 {
 public:
-  explicit goto_symex_statet(const symex_targett::sourcet &);
+  goto_symex_statet(const symex_targett::sourcet &, guard_managert &manager);
   ~goto_symex_statet();
 
   /// \brief Fake "copy constructor" that initializes the `symex_target` member
@@ -58,6 +58,8 @@ class goto_symex_statet final : public goto_statet
   /// for error traces even after symbolic execution has finished.
   symbol_tablet symbol_table;
 
+  // Manager is required to be able to resize the thread vector
+  guard_managert &guard_manager;
   symex_target_equationt *symex_target;
 
   symex_level0t level0;
@@ -155,10 +157,14 @@ class goto_symex_statet final : public goto_statet
   struct threadt
   {
     goto_programt::const_targett pc;
-    guardt guard{true_exprt{}};
+    guardt guard;
     call_stackt call_stack;
     std::map<irep_idt, unsigned> function_frame;
     unsigned atomic_section_id = 0;
+    explicit threadt(guard_managert &guard_manager)
+      : guard(true_exprt(), guard_manager)
+    {
+    }
   };
 
   std::vector<threadt> threads;
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 43dc2d5942d..bca4cf26c02 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -71,8 +71,14 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
     if(state.source.pc->source_location.get_hide())
       assignment_type=symex_targett::assignment_typet::HIDDEN;
 
-    guardt guard{true_exprt{}}; // NOT the state guard!
-    symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
+    exprt::operandst lhs_if_then_else_conditions;
+    symex_assign_rec(
+      state,
+      lhs,
+      nil_exprt(),
+      rhs,
+      lhs_if_then_else_conditions,
+      assignment_type);
   }
 }
 
@@ -115,7 +121,7 @@ void goto_symext::symex_assign_rec(
   const exprt &lhs,
   const exprt &full_lhs,
   const exprt &rhs,
-  guardt &guard,
+  exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   if(lhs.id()==ID_symbol &&
@@ -197,15 +203,15 @@ void goto_symext::symex_assign_symbol(
   const ssa_exprt &lhs, // L1
   const exprt &full_lhs,
   const exprt &rhs,
-  guardt &guard,
+  exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   exprt ssa_rhs=rhs;
 
   // put assignment guard into the rhs
-  if(!guard.is_true())
+  if(!guard.empty())
   {
-    if_exprt tmp_ssa_rhs(guard.as_expr(), ssa_rhs, lhs, ssa_rhs.type());
+    if_exprt tmp_ssa_rhs(conjunction(guard), ssa_rhs, lhs, ssa_rhs.type());
     tmp_ssa_rhs.swap(ssa_rhs);
   }
 
@@ -228,9 +234,6 @@ void goto_symext::symex_assign_symbol(
   exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns);
   state.record_events=record_events;
 
-  guardt tmp_guard(state.guard);
-  tmp_guard.append(guard);
-
   // do the assignment
   const symbolt &symbol =
     ns.lookup(to_symbol_expr(ssa_lhs.get_original_expr()));
@@ -248,14 +251,20 @@ void goto_symext::symex_assign_symbol(
               << messaget::eom;
     });
 
+  // Temporarily add the state guard
+  guard.emplace_back(state.guard.as_expr());
+
   target.assignment(
-    tmp_guard.as_expr(),
+    conjunction(guard),
     ssa_lhs,
     l2_full_lhs,
     add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
     l2_rhs,
     state.source,
     assignment_type);
+
+  // Restore the guard
+  guard.pop_back();
 }
 
 void goto_symext::symex_assign_typecast(
@@ -263,7 +272,7 @@ void goto_symext::symex_assign_typecast(
   const typecast_exprt &lhs,
   const exprt &full_lhs,
   const exprt &rhs,
-  guardt &guard,
+  exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   // these may come from dereferencing on the lhs
@@ -280,7 +289,7 @@ void goto_symext::symex_assign_array(
   const index_exprt &lhs,
   const exprt &full_lhs,
   const exprt &rhs,
-  guardt &guard,
+  exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   const exprt &lhs_array=lhs.array();
@@ -327,7 +336,7 @@ void goto_symext::symex_assign_struct_member(
   const member_exprt &lhs,
   const exprt &full_lhs,
   const exprt &rhs,
-  guardt &guard,
+  exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   // Symbolic execution of a struct member assignment.
@@ -397,30 +406,27 @@ void goto_symext::symex_assign_if(
   const if_exprt &lhs,
   const exprt &full_lhs,
   const exprt &rhs,
-  guardt &guard,
+  exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   // we have (c?a:b)=e;
-
-  guardt old_guard=guard;
-
   exprt renamed_guard = state.rename(lhs.cond(), ns);
   do_simplify(renamed_guard);
 
   if(!renamed_guard.is_false())
   {
-    guard.add(renamed_guard);
+    guard.push_back(renamed_guard);
     symex_assign_rec(
       state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);
-    guard = std::move(old_guard);
+    guard.pop_back();
   }
 
   if(!renamed_guard.is_true())
   {
-    guard.add(not_exprt(renamed_guard));
+    guard.push_back(not_exprt(renamed_guard));
     symex_assign_rec(
       state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
-    guard = std::move(old_guard);
+    guard.pop_back();
   }
 }
 
@@ -429,7 +435,7 @@ void goto_symext::symex_assign_byte_extract(
   const byte_extract_exprt &lhs,
   const exprt &full_lhs,
   const exprt &rhs,
-  guardt &guard,
+  exprt::operandst &guard,
   assignment_typet assignment_type)
 {
   // we have byte_extract_X(object, offset)=value
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 0a43a857ab5..f04e1c21a08 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -134,8 +134,9 @@ void goto_symext::parameter_assignments(
       clean_expr(lhs, state, true);
       clean_expr(rhs, state, false);
 
-      guardt guard{true_exprt{}};
-      symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
+      exprt::operandst lhs_conditions;
+      symex_assign_rec(
+        state, lhs, nil_exprt(), rhs, lhs_conditions, assignment_type);
     }
 
     if(it1!=arguments.end())
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index e569bda6d8a..a47f266f952 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -217,7 +217,7 @@ void goto_symext::symex_goto(statet &state)
   // adjust guards
   if(new_guard.is_true())
   {
-    state.guard = guardt(false_exprt());
+    state.guard = guardt(false_exprt(), guard_manager);
   }
   else
   {
@@ -241,7 +241,7 @@ void goto_symext::symex_goto(statet &state)
         state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns);
       state.assignment(new_lhs, new_rhs, ns, true, false);
 
-      guardt guard{true_exprt{}};
+      guardt guard{true_exprt{}, guard_manager};
 
       log.conditional_output(
         log.debug(),
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 78d9f90ef5d..159d127be30 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -116,8 +116,7 @@ void goto_symext::vcc(
   if(condition.is_true())
     return;
 
-  exprt guarded_condition = condition;
-  state.guard.guard_expr(guarded_condition);
+  const exprt guarded_condition = state.guard.guard_expr(condition);
 
   state.remaining_vccs++;
   target.assertion(state.guard.as_expr(), guarded_condition, msg, state.source);
@@ -146,8 +145,7 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
 
   if(state.threads.size()==1)
   {
-    exprt tmp = rewritten_cond;
-    state.guard.guard_expr(tmp);
+    exprt tmp = state.guard.guard_expr(rewritten_cond);
     target.assumption(state.guard.as_expr(), tmp, state.source);
   }
   // symex_target_equationt::convert_assertions would fail to
@@ -328,7 +326,8 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
 
   // create and prepare the state
   auto state = util_make_unique<statet>(
-    symex_targett::sourcet(entry_point_id, start_function->body));
+    symex_targett::sourcet(entry_point_id, start_function->body),
+    guard_manager);
   CHECK_RETURN(!state->threads.empty());
   CHECK_RETURN(!state->call_stack().empty());
 
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 88c1dfdfa42..2614e0da4f2 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -274,7 +274,7 @@ void goto_symext::symex_other(
     clean_expr(object, state, false);
 
     process_array_expr(state, object);
-    havoc_rec(state, guardt(true_exprt()), object);
+    havoc_rec(state, guardt(true_exprt(), guard_manager), object);
   }
   else
     UNREACHABLE;
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index ddae9b68886..e4e5b8306f6 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -37,7 +37,7 @@ void goto_symext::symex_start_thread(statet &state)
 
   // put into thread vector
   std::size_t t=state.threads.size();
-  state.threads.push_back(statet::threadt());
+  state.threads.push_back(statet::threadt(guard_manager));
   // statet::threadt &cur_thread=state.threads[state.source.thread_nr];
   statet::threadt &new_thread=state.threads.back();
   new_thread.pc=thread_target;
@@ -84,7 +84,7 @@ void goto_symext::symex_start_thread(statet &state)
     // make copy
     ssa_exprt rhs=c_it->second.first;
 
-    guardt guard{true_exprt{}};
+    exprt::operandst lhs_conditions;
     const bool record_events=state.record_events;
     state.record_events=false;
     symex_assign_symbol(
@@ -92,7 +92,7 @@ void goto_symext::symex_start_thread(statet &state)
       lhs_l1,
       nil_exprt(),
       rhs,
-      guard,
+      lhs_conditions,
       symex_targett::assignment_typet::HIDDEN);
     state.record_events=record_events;
   }
@@ -123,13 +123,13 @@ void goto_symext::symex_start_thread(statet &state)
       rhs = *zero;
     }
 
-    guardt guard{true_exprt{}};
+    exprt::operandst lhs_conditions;
     symex_assign_symbol(
       state,
       lhs,
       nil_exprt(),
       rhs,
-      guard,
+      lhs_conditions,
       symex_targett::assignment_typet::HIDDEN);
   }
 }
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index 17fe6b0a547..7b75c1bbfe6 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_code.h>
 #include <util/symbol_table.h>
-#include <util/guard.h>
 #include <util/options.h>
 
 /// \param expr: expression to check
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index cd05d712db0..223b930cded 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -24,7 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
-#include <util/guard.h>
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
diff --git a/src/solvers/bdd/bdd_cudd.h b/src/solvers/bdd/bdd_cudd.h
index c25f4d57c53..01757d75dc6 100644
--- a/src/solvers/bdd/bdd_cudd.h
+++ b/src/solvers/bdd/bdd_cudd.h
@@ -51,10 +51,13 @@ class bdd_nodet
     return bdd_nodet(Cudd_E(node));
   }
 
+  /// Return type for \ref id()
+  using idt = DdNode *;
+
   /// Unique identifier of the node
-  long id() const
+  idt id() const
   {
-    return (long)node;
+    return node;
   }
 
 private:
diff --git a/src/solvers/bdd/bdd_miniBDD.h b/src/solvers/bdd/bdd_miniBDD.h
index fba9dc1a807..d4a04feeefe 100644
--- a/src/solvers/bdd/bdd_miniBDD.h
+++ b/src/solvers/bdd/bdd_miniBDD.h
@@ -55,10 +55,13 @@ class bdd_nodet
     return bdd_nodet(node->low.node, bdd_var_to_index);
   }
 
+  /// Return type for \ref id()
+  using idt = mini_bdd_nodet *;
+
   /// Unique identifier of the node
-  long id() const
+  idt id() const
   {
-    return (long)node;
+    return node;
   }
 
 private:
diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
index 1443a1b8b34..c810f43e080 100644
--- a/src/solvers/prop/bdd_expr.cpp
+++ b/src/solvers/prop/bdd_expr.cpp
@@ -88,12 +88,20 @@ bddt bdd_exprt::from_expr_rec(const exprt &expr)
   }
 }
 
-void bdd_exprt::from_expr(const exprt &expr)
+bddt bdd_exprt::from_expr(const exprt &expr)
 {
-  root=from_expr_rec(expr);
+  return from_expr_rec(expr);
 }
 
-exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const
+/// Helper function for \c bddt to \c exprt conversion
+/// \param r: node to convert
+/// \param complement: whether we want the negation of the expression
+///        represented by r
+/// \param cache: map of already computed values
+exprt bdd_exprt::as_expr(
+  const bdd_nodet &r,
+  bool complement,
+  std::unordered_map<bdd_nodet::idt, exprt> &cache) const
 {
   if(r.is_constant())
   {
@@ -106,50 +114,74 @@ exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const
   INVARIANT(r.index() < node_map.size(), "Index should be in node_map");
   const exprt &n_expr = node_map[r.index()];
 
-  if(r.else_branch().is_constant())
+  // Look-up cache for already computed value
+  auto insert_result = cache.emplace(r.id(), nil_exprt());
+  if(insert_result.second)
   {
-    if(r.then_branch().is_constant())
-    {
-      if(r.else_branch().is_complement() != complement)
-        return n_expr;
-      return not_exprt(n_expr);
-    }
-    else
-    {
-      if(r.else_branch().is_complement() != complement)
+    insert_result.first->second = [&]() -> exprt {
+      if(r.else_branch().is_constant())
+      {
+        if(r.then_branch().is_constant())
+        {
+          if(r.else_branch().is_complement() != complement)
+            return n_expr;
+          return not_exprt(n_expr);
+        }
+        else
+        {
+          if(r.else_branch().is_complement() != complement)
+          {
+            return and_exprt(
+              n_expr,
+              as_expr(
+                r.then_branch(),
+                complement != r.then_branch().is_complement(),
+                cache));
+          }
+          return or_exprt(
+            not_exprt(n_expr),
+            as_expr(
+              r.then_branch(),
+              complement != r.then_branch().is_complement(),
+              cache));
+        }
+      }
+      else if(r.then_branch().is_constant())
       {
-        return and_exprt(
+        if(r.then_branch().is_complement() != complement)
+        {
+          return and_exprt(
+            not_exprt(n_expr),
+            as_expr(
+              r.else_branch(),
+              complement != r.else_branch().is_complement(),
+              cache));
+        }
+        return or_exprt(
           n_expr,
           as_expr(
-            r.then_branch(), complement != r.then_branch().is_complement()));
+            r.else_branch(),
+            complement != r.else_branch().is_complement(),
+            cache));
       }
-      return or_exprt(
-        not_exprt(n_expr),
+      return if_exprt(
+        n_expr,
         as_expr(
-          r.then_branch(), complement != r.then_branch().is_complement()));
-    }
-  }
-  else if(r.then_branch().is_constant())
-  {
-    if(r.then_branch().is_complement() != complement)
-    {
-      return and_exprt(
-        not_exprt(n_expr),
+          r.then_branch(),
+          r.then_branch().is_complement() != complement,
+          cache),
         as_expr(
-          r.else_branch(), complement != r.else_branch().is_complement()));
-    }
-    return or_exprt(
-      n_expr,
-      as_expr(r.else_branch(), complement != r.else_branch().is_complement()));
+          r.else_branch(),
+          r.else_branch().is_complement() != complement,
+          cache));
+    }();
   }
-  return if_exprt(
-    n_expr,
-    as_expr(r.then_branch(), r.then_branch().is_complement() != complement),
-    as_expr(r.else_branch(), r.else_branch().is_complement() != complement));
+  return insert_result.first->second;
 }
 
-exprt bdd_exprt::as_expr() const
+exprt bdd_exprt::as_expr(const bddt &root) const
 {
-  const bdd_nodet node = bdd_mgr.bdd_node(root);
-  return as_expr(node, node.is_complement());
+  std::unordered_map<bdd_nodet::idt, exprt> cache;
+  bdd_nodet node = bdd_mgr.bdd_node(root);
+  return as_expr(node, node.is_complement(), cache);
 }
diff --git a/src/solvers/prop/bdd_expr.h b/src/solvers/prop/bdd_expr.h
index 0314ae4da9d..f8543b659ce 100644
--- a/src/solvers/prop/bdd_expr.h
+++ b/src/solvers/prop/bdd_expr.h
@@ -25,31 +25,33 @@ Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk
 
 #include <unordered_map>
 
-class namespacet;
-
-/*! \brief TO_BE_DOCUMENTED
-*/
+/// Conversion between \c exprt and \c bbdt
+/// This encapsulate a bdd_managert, thus BDDs created with this class should
+/// only be combined with BDDs created using the same instance of
+/// \ref bdd_exprt .
+/// See unit tests in unit/solvers/prop/bdd_expr.cpp for examples.
 class bdd_exprt
 {
 public:
-  explicit bdd_exprt(const namespacet &_ns) : ns(_ns), root(bdd_mgr.bdd_true())
-  {
-  }
-
-  void from_expr(const exprt &expr);
-  exprt as_expr() const;
+  bddt from_expr(const exprt &expr);
+  exprt as_expr(const bddt &root) const;
 
 protected:
-  const namespacet &ns;
   bdd_managert bdd_mgr;
-  bddt root;
 
   typedef std::unordered_map<exprt, bddt, irep_hash> expr_mapt;
+
   expr_mapt expr_map;
+
+  /// Mapping from BDD variables to expressions: the expression at index \c i
+  /// of \p node_map corresponds to the i-th variable
   std::vector<exprt> node_map;
 
   bddt from_expr_rec(const exprt &expr);
-  exprt as_expr(const bdd_nodet &r, bool complement) const;
+  exprt as_expr(
+    const bdd_nodet &r,
+    bool complement,
+    std::unordered_map<bdd_nodet::idt, exprt> &cache) const;
 };
 
 #endif // CPROVER_SOLVERS_PROP_BDD_EXPR_H
diff --git a/src/util/Makefile b/src/util/Makefile
index 8a5f9123c20..8c4c6b5beb4 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -26,7 +26,6 @@ SRC = allocate_objects.cpp \
       fresh_symbol.cpp \
       get_base_name.cpp \
       get_module.cpp \
-      guard.cpp \
       identifier.cpp \
       ieee_float.cpp \
       invariant.cpp \
diff --git a/src/util/guard.h b/src/util/guard.h
deleted file mode 100644
index 7019f9bcce5..00000000000
--- a/src/util/guard.h
+++ /dev/null
@@ -1,57 +0,0 @@
-/*******************************************************************\
-
-Module: Guard Data Structure
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Guard Data Structure
-
-#ifndef CPROVER_UTIL_GUARD_H
-#define CPROVER_UTIL_GUARD_H
-
-#include <iosfwd>
-
-#include "std_expr.h"
-
-class guardt
-{
-public:
-  explicit guardt(const exprt &e) : expr(e)
-  {
-  }
-
-  void add(const exprt &expr);
-
-  void append(const guardt &guard)
-  {
-    add(guard.as_expr());
-  }
-
-  exprt as_expr() const
-  {
-    return expr;
-  }
-
-  void guard_expr(exprt &dest) const;
-
-  bool is_true() const
-  {
-    return expr.is_true();
-  }
-
-  bool is_false() const
-  {
-    return expr.is_false();
-  }
-
-  friend guardt &operator -= (guardt &g1, const guardt &g2);
-  friend guardt &operator |= (guardt &g1, const guardt &g2);
-
-private:
-  exprt expr;
-};
-
-#endif // CPROVER_UTIL_GUARD_H
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
index 2dbdf2c7afb..5e95f88c872 100644
--- a/unit/path_strategies.cpp
+++ b/unit/path_strategies.cpp
@@ -369,6 +369,7 @@ void _check_with_strategy(
 
   REQUIRE(is_valid_path_strategy(strategy));
   std::unique_ptr<path_storaget> worklist = get_path_strategy(strategy);
+  guard_managert guard_manager;
 
   goto_modelt gm;
   int ret;
@@ -385,7 +386,14 @@ void _check_with_strategy(
   safety_checkert::resultt overall_result = safety_checkert::resultt::SAFE;
   std::size_t expected_results_cnt = 0;
 
-  bmct bmc(opts, gm.get_symbol_table(), mh, initial_pc, *worklist, callback);
+  bmct bmc(
+    opts,
+    gm.get_symbol_table(),
+    mh,
+    initial_pc,
+    *worklist,
+    callback,
+    guard_manager);
   safety_checkert::resultt tmp_result = bmc.run(gm);
 
   if(tmp_result != safety_checkert::resultt::PAUSED)
@@ -417,6 +425,7 @@ void _check_with_strategy(
       resume.equation,
       resume.state,
       *worklist,
+      guard_manager,
       callback);
     tmp_result = pe.run(gm);
 
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
index 2eafa4deb96..afcf8bb84c7 100644
--- a/unit/solvers/bdd/miniBDD/miniBDD.cpp
+++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp
@@ -341,12 +341,12 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]")
       REQUIRE(oss.str() == "(a ∧ b) ∨ ¬a");
     }
 
-    bdd_exprt t(ns);
-    t.from_expr(o);
+    bdd_exprt bdd_expr_converter;
+    bddt t = bdd_expr_converter.from_expr(o);
 
     {
       std::ostringstream oss;
-      oss << format(t.as_expr());
+      oss << format(bdd_expr_converter.as_expr(t));
       REQUIRE(oss.str() == "¬a ∨ b");
     }
   }
diff --git a/unit/solvers/prop/bdd_expr.cpp b/unit/solvers/prop/bdd_expr.cpp
index 21eeda5ae97..87ba262e0ea 100644
--- a/unit/solvers/prop/bdd_expr.cpp
+++ b/unit/solvers/prop/bdd_expr.cpp
@@ -20,13 +20,14 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]")
 {
   symbol_tablet symbol_table;
   namespacet ns{symbol_table};
+  bdd_exprt bdd_expr_converter;
 
   GIVEN("A bdd for x&!x")
   {
-    bdd_exprt bdd{ns};
     const symbol_exprt var("x", bool_typet());
-    bdd.from_expr(and_exprt(var, not_exprt(var)));
-    REQUIRE(bdd.as_expr() == false_exprt());
+    const bddt bdd =
+      bdd_expr_converter.from_expr(and_exprt(var, not_exprt(var)));
+    REQUIRE(bdd_expr_converter.as_expr(bdd) == false_exprt());
   }
 
   GIVEN("A bdd for (a&b)|!a")
@@ -34,14 +35,14 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]")
     const symbol_exprt a("a", bool_typet());
     const symbol_exprt b("b", bool_typet());
 
-    bdd_exprt bdd{ns};
-    bdd.from_expr(or_exprt(and_exprt(a, b), not_exprt(a)));
+    const bddt bdd =
+      bdd_expr_converter.from_expr(or_exprt(and_exprt(a, b), not_exprt(a)));
 
     THEN("It is equal to the BDD for (!a|b)")
     {
-      bdd_exprt bdd2{ns};
-      bdd2.from_expr(or_exprt(not_exprt(a), b));
-      REQUIRE(bdd.as_expr() == bdd2.as_expr());
+      const bddt bdd2 = bdd_expr_converter.from_expr(or_exprt(not_exprt(a), b));
+      REQUIRE(
+        bdd_expr_converter.as_expr(bdd) == bdd_expr_converter.as_expr(bdd2));
     }
   }
 
@@ -50,12 +51,11 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]")
     const symbol_exprt a("a", bool_typet());
     const symbol_exprt b("b", bool_typet());
 
-    bdd_exprt bdd{ns};
-    bdd.from_expr(and_exprt(a, not_exprt(b)));
+    const bddt bdd = bdd_expr_converter.from_expr(and_exprt(a, not_exprt(b)));
 
     WHEN("It is converted to an exprt")
     {
-      const exprt result = bdd.as_expr();
+      const exprt result = bdd_expr_converter.as_expr(bdd);
       THEN("It is equal to the expression (a & !b) or (!b & a)")
       {
         REQUIRE(result.id() == ID_and);