diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index 00e20612208..b807563176b 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -653,19 +653,19 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
   exprt &target)
 {
   // First figure out what the appropriate type for this expression is.
-  typet expr_type=nil_typet();
+  optionalt<typet> expr_type;
 
   for(std::map<exprt, exprt>::iterator it=values.begin();
       it!=values.end();
       ++it)
   {
-    if(expr_type==nil_typet())
+    if(!expr_type.has_value())
     {
       expr_type=it->first.type();
     }
     else
     {
-      expr_type=join_types(expr_type, it->first.type());
+      expr_type = join_types(*expr_type, it->first.type());
     }
   }
 
@@ -690,7 +690,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
       it!=coefficients.end();
       ++it)
   {
-    exprt concrete_value=from_integer(1, expr_type);
+    exprt concrete_value = from_integer(1, *expr_type);
 
     for(expr_listt::const_iterator e_it=it->first.begin();
         e_it!=it->first.end();
@@ -701,7 +701,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
       if(e==loop_counter)
       {
         mult_exprt mult(
-          from_integer(num_unwindings, expr_type), concrete_value);
+          from_integer(num_unwindings, *expr_type), concrete_value);
         mult.swap(concrete_value);
       }
       else
@@ -718,7 +718,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
     // OK, concrete_value now contains the value of all the relevant variables
     // multiplied together.  Create the term concrete_value*coefficient and add
     // it into the polynomial.
-    typecast_exprt cast(it->second, expr_type);
+    typecast_exprt cast(it->second, *expr_type);
     const mult_exprt term(concrete_value, cast);
 
     if(rhs.is_nil())
diff --git a/src/goto-instrument/accelerate/polynomial.cpp b/src/goto-instrument/accelerate/polynomial.cpp
index c1e1b63c148..5f9c7a09d8f 100644
--- a/src/goto-instrument/accelerate/polynomial.cpp
+++ b/src/goto-instrument/accelerate/polynomial.cpp
@@ -23,7 +23,7 @@ Author: Matt Lewis
 exprt polynomialt::to_expr()
 {
   exprt ret=nil_exprt();
-  typet itype=nil_typet();
+  optionalt<typet> itype;
 
   // Figure out the appropriate type to do all the intermediate calculations
   // in.
@@ -35,13 +35,13 @@ exprt polynomialt::to_expr()
         t_it!=m_it->terms.end();
         ++t_it)
     {
-      if(itype==nil_typet())
+      if(itype.has_value())
       {
         itype=t_it->var.type();
       }
       else
       {
-        itype=join_types(itype, t_it->var.type());
+        itype = join_types(*itype, t_it->var.type());
       }
     }
   }
@@ -59,7 +59,7 @@ exprt polynomialt::to_expr()
       coeff=-coeff;
     }
 
-    exprt mon_expr=from_integer(coeff, itype);
+    exprt mon_expr = from_integer(coeff, *itype);
 
     for(std::vector<monomialt::termt>::iterator t_it=m_it->terms.begin();
         t_it!=m_it->terms.end();
@@ -67,7 +67,7 @@ exprt polynomialt::to_expr()
     {
       for(unsigned int i=0; i < t_it->exp; i++)
       {
-        mon_expr=mult_exprt(mon_expr, typecast_exprt(t_it->var, itype));
+        mon_expr = mult_exprt(mon_expr, typecast_exprt(t_it->var, *itype));
       }
     }
 
@@ -75,7 +75,7 @@ exprt polynomialt::to_expr()
     {
       if(neg)
       {
-        ret=unary_minus_exprt(mon_expr, itype);
+        ret = unary_minus_exprt(mon_expr, *itype);
       }
       else
       {
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 2330e0eda59..28dc7f720bf 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -508,7 +508,7 @@ void polynomial_acceleratort::assert_for_values(
   overflow_instrumentert &overflow)
 {
   // First figure out what the appropriate type for this expression is.
-  typet expr_type=nil_typet();
+  optionalt<typet> expr_type;
 
   for(std::map<exprt, int>::iterator it=values.begin();
       it!=values.end();
@@ -523,25 +523,26 @@ void polynomial_acceleratort::assert_for_values(
       this_type=size_type();
     }
 
-    if(expr_type==nil_typet())
+    if(!expr_type.has_value())
     {
       expr_type=this_type;
     }
     else
     {
-      expr_type=join_types(expr_type, this_type);
+      expr_type = join_types(*expr_type, this_type);
     }
   }
 
-  assert(to_bitvector_type(expr_type).get_width()>0);
-
+  INVARIANT(
+    to_bitvector_type(*expr_type).get_width() > 0,
+    "joined types must be non-empty bitvector types");
 
   // Now set the initial values of the all the variables...
   for(std::map<exprt, int>::iterator it=values.begin();
       it!=values.end();
       ++it)
   {
-    program.assign(it->first, from_integer(it->second, expr_type));
+    program.assign(it->first, from_integer(it->second, *expr_type));
   }
 
   // Now unwind the loop as many times as we need to.
@@ -583,8 +584,8 @@ void polynomial_acceleratort::assert_for_values(
     // OK, concrete_value now contains the value of all the relevant variables
     // multiplied together.  Create the term concrete_value*coefficient and add
     // it into the polynomial.
-    typecast_exprt cast(it->second, expr_type);
-    const mult_exprt term(from_integer(concrete_value, expr_type), cast);
+    typecast_exprt cast(it->second, *expr_type);
+    const mult_exprt term(from_integer(concrete_value, *expr_type), cast);
 
     if(rhs.is_nil())
     {