diff --git a/src/ebmc/output_verilog.cpp b/src/ebmc/output_verilog.cpp
index f71e49275..3ce5a0dd1 100644
--- a/src/ebmc/output_verilog.cpp
+++ b/src/ebmc/output_verilog.cpp
@@ -6,20 +6,22 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <cstdlib>
-#include <iostream>
+#include <verilog/expr2verilog_class.h>
 
 #include <util/ebmc_util.h>
+#include <util/mathematical_expr.h>
 #include <util/simplify_expr.h>
 
+#include <verilog/expr2verilog.h>
 #include <verilog/verilog_language.h>
-#include <verilog/verilog_typecheck.h>
 #include <verilog/verilog_synthesis.h>
-#include <verilog/expr2verilog_class.h>
-#include <verilog/expr2verilog.h>
+#include <verilog/verilog_typecheck.h>
 
 #include "output_verilog.h"
 
+#include <cstdlib>
+#include <iostream>
+
 /*******************************************************************\
 
 Function: output_verilog_baset::width
@@ -41,8 +43,8 @@ std::size_t output_verilog_baset::width(const typet &type)
     return to_bitvector_type(type).get_width();
   
   std::cerr << type.id() << '\n';
-  assert(false);
-  
+  PRECONDITION(false);
+
   return 0; // not reached
 }
 
@@ -165,8 +167,10 @@ void output_verilog_netlistt::assign_symbol(
           rhs.id()==ID_xor ||
           rhs.id()==ID_xnor)
   {
-    assert(rhs.type().id()==ID_bool);
-    assert(lhs.type().id()==ID_bool);
+    DATA_INVARIANT(
+      rhs.type().id() == ID_bool, "boolean equivalence rhs must be boolean");
+    DATA_INVARIANT(
+      lhs.type().id() == ID_bool, "boolean equivalence lhs must be boolean");
 
     std::string tmp;
     
@@ -182,8 +186,10 @@ void output_verilog_netlistt::assign_symbol(
   }
   else if(rhs.id()==ID_not)
   {
-    assert(rhs.type().id()==ID_bool);
-    assert(lhs.type().id()==ID_bool);
+    DATA_INVARIANT(
+      rhs.type().id() == ID_bool, "boolean equivalence rhs must be boolean");
+    DATA_INVARIANT(
+      lhs.type().id() == ID_bool, "boolean equivalence lhs must be boolean");
 
     std::string tmp = make_symbol_expr(to_not_expr(rhs).op(), "");
 
@@ -201,7 +207,8 @@ void output_verilog_netlistt::assign_symbol(
     {
       std::string tmp;
 
-      assert(rhs.operands().size()!=0);
+      DATA_INVARIANT(
+        rhs.operands().size() != 0, "multi-ary operator must have operand");
 
       if(rhs.operands().size()==2)
         tmp = make_symbol_expr(to_multi_ary_expr(rhs).op0(), "") + ", " +
@@ -420,7 +427,7 @@ std::string output_verilog_netlistt::symbol_string(const exprt &expr)
 
     std::size_t offset = atoi(src.type().get("#offset").c_str());
 
-    assert(i>=offset);
+    DATA_INVARIANT(i >= offset, "extractbit index must be in range");
 
     return symbol_string(src) + '[' + integer2string(i - offset) + ']';
   }
@@ -440,10 +447,10 @@ std::string output_verilog_netlistt::symbol_string(const exprt &expr)
     auto to = from + width(expr.type());
     std::size_t offset = atoi(src.type().get("#offset").c_str());
 
-    assert(from>=offset);
-    assert(to>=offset);
-    
-    assert(to>=from);
+    DATA_INVARIANT(from >= offset, "extractbits index must be in range");
+    DATA_INVARIANT(to >= offset, "extractbits index must be in range");
+
+    DATA_INVARIANT(to >= from, "extractbits index must be in range");
 
     return symbol_string(src) + '[' + integer2string(to - offset) + ':' +
            integer2string(from - offset) + ']';
@@ -804,7 +811,7 @@ Function: output_verilog_baset::module_instantiation
 
 void output_verilog_baset::module_instantiation(const exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
+  PRECONDITION(expr.type().id() == ID_bool);
 
   std::list<std::string> argument_strings;
 
@@ -852,8 +859,8 @@ Function: output_verilog_baset::invariant
 
 void output_verilog_baset::invariant(const exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
-  
+  PRECONDITION(expr.type().id() == ID_bool);
+
   if(expr.id()==ID_and)
   {
     forall_operands(it, expr)
@@ -894,10 +901,9 @@ Function: output_verilog_baset::invariants
 
 void output_verilog_baset::invariants(const symbolt &symbol)
 {
-  assert(symbol.value.id()==ID_trans &&
-         symbol.value.operands().size()==3);
+  PRECONDITION(symbol.value.id() == ID_trans);
 
-  invariant(to_ternary_expr(symbol.value).op0());
+  invariant(to_trans_expr(symbol.value).invar());
 }
 
 /*******************************************************************\
@@ -914,8 +920,8 @@ Function: output_verilog_baset::next_state
 
 void output_verilog_baset::next_state(const exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
-  
+  PRECONDITION(expr.type().id() == ID_bool);
+
   if(expr.id()==ID_and)
   {
     forall_operands(it, expr)
@@ -925,7 +931,8 @@ void output_verilog_baset::next_state(const exprt &expr)
   else if(expr.is_true())
     return;
 
-  assert(expr.id()==ID_equal);
+  DATA_INVARIANT(
+    expr.id() == ID_equal, "next-state constraints must be equality");
 
   auto &equal_expr = to_equal_expr(expr);
   assign_symbol(equal_expr.lhs(), equal_expr.rhs());
@@ -945,10 +952,9 @@ Function: output_verilog_baset::next_state
 
 void output_verilog_baset::next_state(const symbolt &symbol)
 {
-  assert(symbol.value.id()==ID_trans &&
-         symbol.value.operands().size()==3);
+  PRECONDITION(symbol.value.id() == ID_trans);
 
-  next_state(symbol.value.operands()[2]);
+  next_state(to_trans_expr(symbol.value).trans());
 }
 
 /*******************************************************************\
diff --git a/src/trans-netlist/aig_prop.h b/src/trans-netlist/aig_prop.h
index c2a1a102f..1d18be4d3 100644
--- a/src/trans-netlist/aig_prop.h
+++ b/src/trans-netlist/aig_prop.h
@@ -9,10 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_TRANS_NETLIST_AIG_PROP_H
 #define CPROVER_TRANS_NETLIST_AIG_PROP_H
 
-#include <cassert>
+#include <util/invariant.h>
+#include <util/threeval.h>
 
 #include <solvers/prop/prop.h>
-#include <util/threeval.h>
 
 #include "aig.h"
 
@@ -28,7 +28,10 @@ class aig_prop_baset : public propt {
   literalt lor(literalt a, literalt b) override;
   literalt land(const bvt &bv) override;
   literalt lor(const bvt &bv) override;
-  void lcnf(const bvt &clause) override { assert(false); }
+  void lcnf(const bvt &clause) override
+  {
+    PRECONDITION(false);
+  }
   literalt lxor(literalt a, literalt b) override;
   literalt lxor(const bvt &bv) override;
   literalt lnand(literalt a, literalt b) override;
@@ -38,7 +41,10 @@ class aig_prop_baset : public propt {
   literalt lselect(literalt a, literalt b, literalt c) override; // a?b:c
   void set_equal(literalt a, literalt b) override;
 
-  void l_set_to(literalt a, bool value) override { assert(false); }
+  void l_set_to(literalt a, bool value) override
+  {
+    PRECONDITION(false);
+  }
 
   literalt new_variable() override { return dest.new_node(); }
 
@@ -49,12 +55,12 @@ class aig_prop_baset : public propt {
   }
 
   tvt l_get(literalt a) const override {
-    assert(0);
+    PRECONDITION(false);
     return tvt::unknown();
   }
 
   resultt prop_solve() {
-    assert(0);
+    PRECONDITION(false);
     return resultt::P_ERROR;
   }
 
diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp
index 960a23314..48cc61d72 100644
--- a/src/trans-netlist/trans_to_netlist.cpp
+++ b/src/trans-netlist/trans_to_netlist.cpp
@@ -532,7 +532,7 @@ void convert_trans_to_netlistt::convert_lhs_rec(
   std::size_t from, std::size_t to,
   propt &prop)
 {
-  assert(from<=to);
+  PRECONDITION(from <= to);
 
   if(expr.id()==ID_symbol)
   { 
@@ -629,11 +629,11 @@ literalt convert_trans_to_netlistt::convert_rhs(
     instantiate_convert(
       prop, dest.var_map, rhs_entry.expr, ns,
       get_message_handler(), rhs_entry.bv);
-      
-    assert(rhs_entry.bv.size()==rhs_entry.width);
+
+    DATA_INVARIANT(rhs_entry.bv.size() == rhs_entry.width, "bit-width match");
   }
 
-  assert(rhs.bit_number<rhs_entry.bv.size());
+  DATA_INVARIANT(rhs.bit_number < rhs_entry.bv.size(), "bit index in range");
   return rhs_entry.bv[rhs.bit_number];
 }
 
@@ -665,12 +665,12 @@ void convert_trans_to_netlistt::add_equality(const equal_exprt &src)
     constraint_list.push_back(src);
     return;
   }
-  
-  assert(rhs_entry.width!=0);
+
+  DATA_INVARIANT(rhs_entry.width != 0, "no empty entries");
 
   std::size_t lhs_width=boolbv_width(lhs.type());
 
-  assert(lhs_width==rhs_entry.width);
+  DATA_INVARIANT(lhs_width == rhs_entry.width, "bit-width match");
 
   add_equality_rec(src, lhs, 0, lhs_width-1, rhs_entry);
 }
@@ -693,8 +693,8 @@ void convert_trans_to_netlistt::add_equality_rec(
   std::size_t lhs_from, std::size_t lhs_to,
   rhs_entryt &rhs_entry)
 {
-  assert(lhs_from<=lhs_to);
-  
+  PRECONDITION(lhs_from <= lhs_to);
+
   if(lhs.id()==ID_next_symbol ||
      lhs.id()==ID_symbol)
   { 
@@ -730,11 +730,11 @@ void convert_trans_to_netlistt::add_equality_rec(
   }
   else if(lhs.id()==ID_extractbit)
   {
-    assert(lhs_to==lhs_from);
+    PRECONDITION(lhs_to == lhs_from);
 
     mp_integer i;
     if(to_integer_non_constant(to_extractbit_expr(lhs).index(), i))
-      assert(false);
+      PRECONDITION(false);
 
     lhs_from = lhs_from + i.to_ulong();
     add_equality_rec(
diff --git a/src/trans-word-level/counterexample_word_level.cpp b/src/trans-word-level/counterexample_word_level.cpp
index af8ce41cb..47bbd39be 100644
--- a/src/trans-word-level/counterexample_word_level.cpp
+++ b/src/trans-word-level/counterexample_word_level.cpp
@@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <cassert>
 #include <iostream>
 
 #include <langapi/language_util.h>
diff --git a/src/trans-word-level/instantiate_word_level.cpp b/src/trans-word-level/instantiate_word_level.cpp
index 77656cc2b..6965c0e69 100644
--- a/src/trans-word-level/instantiate_word_level.cpp
+++ b/src/trans-word-level/instantiate_word_level.cpp
@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "property.h"
 
-#include <cassert>
-
 /*******************************************************************\
 
 Function: timeframe_identifier
@@ -166,7 +164,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
 
       if(sva_cycle_delay_expr.to().id() == ID_infinity)
       {
-        assert(no_timeframes != 0);
+        DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
         to = no_timeframes - 1;
       }
       else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
@@ -283,9 +281,6 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
           expr.id()==ID_sva_s_until)
   {
     // non-overlapping until
-  
-    assert(expr.operands().size()==2);
-    
     // we need a lasso to refute these
 
     // we expand: p U q <=> q || (p && X(p U q))
@@ -308,8 +303,6 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
           expr.id()==ID_sva_s_until_with)
   {
     // overlapping until
-  
-    assert(expr.operands().size()==2);
     
     // we rewrite using 'next'
     binary_exprt tmp = to_binary_expr(expr);
diff --git a/src/verilog/verilog_typecheck_base.cpp b/src/verilog/verilog_typecheck_base.cpp
index ddc461383..fe9d73dc8 100644
--- a/src/verilog/verilog_typecheck_base.cpp
+++ b/src/verilog/verilog_typecheck_base.cpp
@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "expr2verilog.h"
 #include "verilog_types.h"
 
-#include <cassert>
-
 /*******************************************************************\
 
 Function: verilog_module_symbol
@@ -50,8 +48,10 @@ Function: strip_verilog_prefix
 irep_idt strip_verilog_prefix(const irep_idt &identifier)
 {
   std::string prefix="Verilog::";
-  assert(has_prefix(id2string(identifier), prefix));
-  assert(identifier.size()>=prefix.size());
+  DATA_INVARIANT(
+    has_prefix(id2string(identifier), prefix), "Verilog identifier syntax");
+  DATA_INVARIANT(
+    identifier.size() >= prefix.size(), "Verilog identifier syntax");
   return identifier.c_str()+prefix.size();
 }
 
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 4917c976b..74285f441 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -1553,7 +1553,7 @@ void verilog_typecheck_exprt::implicit_typecast(
       {
         const std::string &value=expr.get_string(ID_value);
         // least significant bit is last
-        assert(value.size()!=0);
+        DATA_INVARIANT(value.size() != 0, "no empty bitvector");
         expr = make_boolean_expr(value[value.size() - 1] == '1');
         return;
       }
@@ -1860,7 +1860,6 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak ||
     expr.id() == ID_sva_strong)
   {
-    assert(expr.operands().size()==1);
     convert_expr(expr.op());
     make_boolean(expr.op());
     expr.type()=bool_typet();
@@ -2163,7 +2162,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   else if(expr.id()==ID_ashr)
   {
     // would only happen when re-typechecking, otherwise see above
-    assert(0);
+    DATA_INVARIANT(false, "no re-typechecking");
   }
   else if(expr.id()==ID_lshr)
   {
@@ -2452,7 +2451,6 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
   else if(expr.id()==ID_sva_cycle_delay) // #[1:2] something
   {
     expr.type()=bool_typet();
-    assert(expr.operands().size()==3);
     convert_expr(expr.op0());
     if(expr.op1().is_not_nil()) convert_expr(expr.op1());
     convert_expr(expr.op2());
diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
index 27b601eee..dd866411d 100644
--- a/src/verilog/verilog_typecheck_expr.h
+++ b/src/verilog/verilog_typecheck_expr.h
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "verilog_typecheck_base.h"
 
-#include <cassert>
 #include <stack>
 
 class function_call_exprt;
@@ -110,7 +109,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   // To be overridden, requires a Verilog interpreter.
   virtual exprt elaborate_constant_function_call(const function_call_exprt &)
   {
-    assert(false);
+    UNREACHABLE;
   }
 
 private: