From 16d03d7217162f8b7e469daa5bc387d48e29fcc3 Mon Sep 17 00:00:00 2001
From: John Nonweiler <john.nonweiler@diffblue.com>
Date: Tue, 10 Jul 2018 17:00:12 +0100
Subject: [PATCH 1/9] Replace asserts and throws with INVARIANT etc.

---
 src/goto-symex/build_goto_trace.cpp          |  4 +++-
 src/goto-symex/goto_symex_state.cpp          |  4 ++--
 src/goto-symex/memory_model_pso.cpp          |  4 ++--
 src/goto-symex/memory_model_sc.cpp           |  4 ++--
 src/goto-symex/memory_model_tso.cpp          |  4 ++--
 src/goto-symex/partial_order_concurrency.cpp |  4 ++--
 src/goto-symex/postcondition.cpp             | 15 ++++++++++-----
 src/goto-symex/precondition.cpp              | 15 ++++++++++-----
 src/goto-symex/slice.cpp                     |  4 ++--
 src/goto-symex/symex_assign.cpp              | 15 ++++++++-------
 10 files changed, 43 insertions(+), 30 deletions(-)

diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 648583605af..83a6a08838a 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -92,7 +92,9 @@ exprt build_full_lhs_rec(
           id==ID_byte_extract_big_endian)
   {
     exprt tmp=src_original;
-    assert(tmp.operands().size()==2);
+    DATA_INVARIANT(
+      tmp.operands().size() == 2,
+      "byte_extract_exprt should have two operands.");
     tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
 
     // re-write into big case-split
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index e306a86d13d..7403238a395 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -187,8 +187,8 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   }
   else if(expr.id()==ID_member)
   {
-    if(expr.operands().size()!=1)
-      throw "member expects one operand";
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "member_exprt takes one operand.");
 
     return constant_propagation_reference(expr.op0());
   }
diff --git a/src/goto-symex/memory_model_pso.cpp b/src/goto-symex/memory_model_pso.cpp
index d8487e629fd..729d47eabb0 100644
--- a/src/goto-symex/memory_model_pso.cpp
+++ b/src/goto-symex/memory_model_pso.cpp
@@ -30,8 +30,8 @@ bool memory_model_psot::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(e1->is_shared_read() || e1->is_shared_write());
-  assert(e2->is_shared_read() || e2->is_shared_write());
+  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
+  PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
 
   // no po relaxation within atomic sections
   if(e1->atomic_section_id!=0 &&
diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp
index a09f9652f30..9575a09c920 100644
--- a/src/goto-symex/memory_model_sc.cpp
+++ b/src/goto-symex/memory_model_sc.cpp
@@ -36,8 +36,8 @@ bool memory_model_sct::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(e1->is_shared_read() || e1->is_shared_write());
-  assert(e2->is_shared_read() || e2->is_shared_write());
+  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
+  PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
 
   return false;
 }
diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp
index 8bf28a28813..2d05a76b00f 100644
--- a/src/goto-symex/memory_model_tso.cpp
+++ b/src/goto-symex/memory_model_tso.cpp
@@ -39,8 +39,8 @@ bool memory_model_tsot::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(e1->is_shared_read() || e1->is_shared_write());
-  assert(e2->is_shared_read() || e2->is_shared_write());
+  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
+  PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
 
   // no po relaxation within atomic sections
   if(e1->atomic_section_id!=0 &&
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index fb9529a83fb..22cbc2f538a 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -143,7 +143,7 @@ symbol_exprt partial_order_concurrencyt::clock(
   axiomt axiom)
 {
   irep_idt identifier;
-  assert(!numbering.empty());
+  PRECONDITION(!numbering.empty());
 
   if(event->is_shared_write())
     identifier=rw_clock_id(event, axiom);
@@ -163,7 +163,7 @@ symbol_exprt partial_order_concurrencyt::clock(
 
 void partial_order_concurrencyt::build_clock_type()
 {
-  assert(!numbering.empty());
+  PRECONDITION(!numbering.empty());
 
   std::size_t width = address_bits(numbering.size());
   clock_type = unsignedbv_typet(width);
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 57624a25d56..347b527d51c 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -76,7 +76,8 @@ bool postconditiont::is_used_address_of(
   }
   else if(expr.id()==ID_index)
   {
-    assert(expr.operands().size()==2);
+    DATA_INVARIANT(
+      expr.operands().size() == 2, "index_exprt takes two operands.");
 
     return
       is_used_address_of(expr.op0(), identifier) ||
@@ -84,12 +85,14 @@ bool postconditiont::is_used_address_of(
   }
   else if(expr.id()==ID_member)
   {
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "member_exprt takes one operand.");
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_dereference)
   {
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "dereference_exprt takes one operand.");
     return is_used(expr.op0(), identifier);
   }
 
@@ -155,7 +158,8 @@ bool postconditiont::is_used(
   if(expr.id()==ID_address_of)
   {
     // only do index!
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "address_of_exprt takes one operand.");
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_symbol &&
@@ -169,7 +173,8 @@ bool postconditiont::is_used(
   }
   else if(expr.id()==ID_dereference)
   {
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "dereference_exprt takes one operand.");
 
     // aliasing may happen here
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 69d26cd19f6..d7bd35b37e2 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -78,18 +78,21 @@ void preconditiont::compute_address_of(exprt &dest)
   }
   else if(dest.id()==ID_index)
   {
-    assert(dest.operands().size()==2);
+    DATA_INVARIANT(
+      dest.operands().size() == 2, "index_exprt takes two operands.");
     compute_address_of(dest.op0());
     compute(dest.op1());
   }
   else if(dest.id()==ID_member)
   {
-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+      dest.operands().size() == 1, "member_exprt takes one operand.");
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+      dest.operands().size() == 1, "dereference_exprt takes one operand.");
     compute(dest.op0());
   }
 }
@@ -104,12 +107,14 @@ void preconditiont::compute_rec(exprt &dest)
   if(dest.id()==ID_address_of)
   {
     // only do index!
-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+      dest.operands().size() == 1, "address_of_exprt takes one operand.");
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+      dest.operands().size() == 1, "dereference_exprt takes one operand.");
 
     const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
 
diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
index 654c45bbb68..de35a1c421d 100644
--- a/src/goto-symex/slice.cpp
+++ b/src/goto-symex/slice.cpp
@@ -112,7 +112,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
 void symex_slicet::slice_assignment(
   symex_target_equationt::SSA_stept &SSA_step)
 {
-  assert(SSA_step.ssa_lhs.id()==ID_symbol);
+  PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
   const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
 
   if(depends.find(id)==depends.end())
@@ -127,7 +127,7 @@ void symex_slicet::slice_assignment(
 void symex_slicet::slice_decl(
   symex_target_equationt::SSA_stept &SSA_step)
 {
-  assert(SSA_step.ssa_lhs.id()==ID_symbol);
+  PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
   const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
 
   if(depends.find(id)==depends.end())
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index ce5d7ee0775..b96d79fc417 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -91,7 +91,7 @@ exprt goto_symext::add_to_lhs(
   const exprt &lhs,
   const exprt &what)
 {
-  assert(lhs.id()!=ID_symbol);
+  PRECONDITION(lhs.id() != ID_symbol);
   exprt tmp_what=what;
 
   if(tmp_what.id()!=ID_symbol)
@@ -172,7 +172,9 @@ void goto_symext::symex_assign_rec(
           lhs.id()==ID_complex_imag)
   {
     // this is stuff like __real__ x = 1;
-    assert(lhs.operands().size()==1);
+    DATA_INVARIANT(
+      lhs.operands().size() == 1,
+      "exprts with id ID_complex_real or ID_complex_imag take one operand.");
 
     exprt new_rhs=exprt(ID_complex, lhs.op0().type());
     new_rhs.operands().resize(2);
@@ -283,7 +285,7 @@ void goto_symext::symex_assign_typecast(
 {
   // these may come from dereferencing on the lhs
 
-  assert(lhs.operands().size()==1);
+  PRECONDITION(lhs.operands().size() == 1);
 
   exprt rhs_typecasted=rhs;
   rhs_typecasted.make_typecast(lhs.op0().type());
@@ -305,9 +307,7 @@ void goto_symext::symex_assign_array(
   // lhs must be index operand
   // that takes two operands: the first must be an array
   // the second is the index
-
-  if(lhs.operands().size()!=2)
-    throw "index must have two operands";
+  DATA_INVARIANT(lhs.operands().size() == 2, "index_exprt takes two operands");
 
   const exprt &lhs_array=lhs.array();
   const exprt &lhs_index=lhs.index();
@@ -368,7 +368,8 @@ void goto_symext::symex_assign_struct_member(
   // typecasts involved? C++ does that for inheritance.
   if(lhs_struct.id()==ID_typecast)
   {
-    assert(lhs_struct.operands().size()==1);
+    DATA_INVARIANT(
+      lhs_struct.operands().size() == 1, "typecast_exprt takes one operand.");
 
     if(lhs_struct.op0().id() == ID_null_object)
     {

From 526945e435a9f42d6579a7a0897159ba5434c09e Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 19 Jul 2018 10:27:48 +0100
Subject: [PATCH 2/9] Translate asserts and throws to PRECONDITIONS and
 INVARIANTS

---
 src/goto-symex/build_goto_trace.cpp          |  6 +-
 src/goto-symex/goto_symex_state.cpp          | 13 +--
 src/goto-symex/partial_order_concurrency.cpp |  2 +-
 src/goto-symex/postcondition.cpp             | 16 ++--
 src/goto-symex/precondition.cpp              | 15 ++--
 src/goto-symex/slice_by_trace.cpp            | 15 +++-
 src/goto-symex/symex_assign.cpp              | 21 +++--
 src/goto-symex/symex_atomic_section.cpp      | 13 ++-
 src/goto-symex/symex_builtin_functions.cpp   | 84 ++++++++------------
 src/goto-symex/symex_dead.cpp                |  9 +--
 src/goto-symex/symex_decl.cpp                | 13 ++-
 src/goto-symex/symex_dereference.cpp         |  4 +-
 src/goto-symex/symex_function_call.cpp       | 48 +++++------
 src/goto-symex/symex_goto.cpp                |  7 +-
 src/goto-symex/symex_main.cpp                |  6 +-
 src/goto-symex/symex_other.cpp               | 15 ++--
 src/goto-symex/symex_start_thread.cpp        |  8 +-
 17 files changed, 120 insertions(+), 175 deletions(-)

diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 83a6a08838a..1a20a5266e0 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -92,9 +92,7 @@ exprt build_full_lhs_rec(
           id==ID_byte_extract_big_endian)
   {
     exprt tmp=src_original;
-    DATA_INVARIANT(
-      tmp.operands().size() == 2,
-      "byte_extract_exprt should have two operands.");
+    PRECONDITION(tmp.operands().size() == 2);
     tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
 
     // re-write into big case-split
@@ -224,7 +222,7 @@ void build_goto_trace(
       else if(it->is_atomic_end() && current_time<0)
         current_time*=-1;
 
-      assert(current_time>=0);
+      PRECONDITION(current_time>=0);
       // move any steps gathered in an atomic section
 
       if(time_before<0)
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 7403238a395..0af0547490b 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -51,8 +51,7 @@ void goto_symex_statet::level0t::operator()(
 
   const symbolt *s;
   const bool found_l0 = !ns.lookup(obj_identifier, s);
-  DATA_INVARIANT(
-    found_l0, "level0: failed to find " + id2string(obj_identifier));
+  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id()==ID_code ||
@@ -187,8 +186,7 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   }
   else if(expr.id()==ID_member)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "member_exprt takes one operand.");
+    PRECONDITION(expr.operands().size() == 1);
 
     return constant_propagation_reference(expr.op0());
   }
@@ -495,12 +493,9 @@ void goto_symex_statet::rename(
   }
   else if(expr.id()==ID_address_of)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "address_of should have a single operand");
+    PRECONDITION(expr.operands().size() == 1);
     rename_address(expr.op0(), ns, level);
-    DATA_INVARIANT(
-      expr.type().id() == ID_pointer,
-      "type of address_of should be ID_pointer");
+    PRECONDITION(expr.type().id() == ID_pointer);
     expr.type().subtype()=expr.op0().type();
   }
   else
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index 22cbc2f538a..49204e1c678 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -198,7 +198,7 @@ exprt partial_order_concurrencyt::before(
         binary_relation_exprt(clock(e1, ax), ID_lt, clock(e2, ax)));
   }
 
-  assert(!ops.empty());
+  POSTCONDITION(!ops.empty());
 
   return conjunction(ops);
 }
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 347b527d51c..462417871e8 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -76,23 +76,19 @@ bool postconditiont::is_used_address_of(
   }
   else if(expr.id()==ID_index)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 2, "index_exprt takes two operands.");
-
+    PRECONDITION(expr.operands().size() == 2);
     return
       is_used_address_of(expr.op0(), identifier) ||
       is_used(expr.op1(), identifier);
   }
   else if(expr.id()==ID_member)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "member_exprt takes one operand.");
+    PRECONDITION(expr.operands().size() == 1);
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_dereference)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "dereference_exprt takes one operand.");
+    PRECONDITION(expr.operands().size() == 1);
     return is_used(expr.op0(), identifier);
   }
 
@@ -158,8 +154,7 @@ bool postconditiont::is_used(
   if(expr.id()==ID_address_of)
   {
     // only do index!
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "address_of_exprt takes one operand.");
+    PRECONDITION(expr.operands().size() == 1);
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_symbol &&
@@ -173,8 +168,7 @@ bool postconditiont::is_used(
   }
   else if(expr.id()==ID_dereference)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "dereference_exprt takes one operand.");
+    PRECONDITION(expr.operands().size() == 1);
 
     // aliasing may happen here
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index d7bd35b37e2..111d3e339f5 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -78,21 +78,18 @@ void preconditiont::compute_address_of(exprt &dest)
   }
   else if(dest.id()==ID_index)
   {
-    DATA_INVARIANT(
-      dest.operands().size() == 2, "index_exprt takes two operands.");
+    PRECONDITION(dest.operands().size() == 2);
     compute_address_of(dest.op0());
     compute(dest.op1());
   }
   else if(dest.id()==ID_member)
   {
-    DATA_INVARIANT(
-      dest.operands().size() == 1, "member_exprt takes one operand.");
+    PRECONDITION(dest.operands().size() == 1);
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
-    DATA_INVARIANT(
-      dest.operands().size() == 1, "dereference_exprt takes one operand.");
+    PRECONDITION(dest.operands().size() == 1);
     compute(dest.op0());
   }
 }
@@ -107,14 +104,12 @@ void preconditiont::compute_rec(exprt &dest)
   if(dest.id()==ID_address_of)
   {
     // only do index!
-    DATA_INVARIANT(
-      dest.operands().size() == 1, "address_of_exprt takes one operand.");
+    PRECONDITION(dest.operands().size() == 1);
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
-    DATA_INVARIANT(
-      dest.operands().size() == 1, "dereference_exprt takes one operand.");
+    PRECONDITION(dest.operands().size() == 1);
 
     const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
 
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index d02b54ed3e7..36056617674 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -79,6 +79,13 @@ void symex_slice_by_tracet::slice_by_trace(
   {
     exprt g_copy(*i);
 
+    INVARIANT(
+    	g_copy.id() == ID_symbol || 
+    	g_copy.id() == ID_not ||
+    	g_copy.id() == ID_and ||
+    	g_copy.id() == ID_constant,
+    	"guards should only be and, symbol, constant, or `not'");
+
     if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
     {
       g_copy.make_not();
@@ -94,7 +101,7 @@ void symex_slice_by_tracet::slice_by_trace(
     }
     else if(!(g_copy.id()==ID_constant))
     {
-      throw "guards should only be and, symbol, constant, or `not'";
+      UNHANDLED_CASE;
     }
   }
 
@@ -219,9 +226,9 @@ void symex_slice_by_tracet::parse_events(std::string read_line)
     const std::string::size_type vnext=read_line.find(",", vidx);
     std::string event=read_line.substr(vidx, vnext - vidx);
     eis.insert(event);
-    if((!alphabet.empty()) &&
-       ((alphabet.count(event)!=0)!=alphabet_parity))
-      throw "trace uses symbol not in alphabet: "+event;
+    PRECONDITION(!alphabet.empty());
+    INVARIANT((alphabet.count(event) != 0) == alphabet_parity, 
+    	"trace uses symbol not in alphabet: " + event);
     if(vnext==std::string::npos)
       break;
     vidx=vnext;
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index b96d79fc417..5292e0492d4 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -37,7 +37,7 @@ void goto_symext::symex_assign(
 
     if(statement==ID_function_call)
     {
-      assert(!side_effect_expr.operands().empty());
+      PRECONDITION(!side_effect_expr.operands().empty());
 
       if(side_effect_expr.op0().id()!=ID_symbol)
         throw "symex_assign: expected symbol as function";
@@ -96,7 +96,7 @@ exprt goto_symext::add_to_lhs(
 
   if(tmp_what.id()!=ID_symbol)
   {
-    assert(tmp_what.operands().size()>=1);
+    PRECONDITION(tmp_what.operands().size() >= 1);
     tmp_what.op0().make_nil();
   }
 
@@ -106,12 +106,12 @@ exprt goto_symext::add_to_lhs(
 
   while(p->is_not_nil())
   {
-    assert(p->id()!=ID_symbol);
-    assert(p->operands().size()>=1);
+    PRECONDITION(p->id()!=ID_symbol);
+    PRECONDITION(p->operands().size()>=1);
     p=&p->op0();
   }
 
-  assert(p->is_nil());
+  PRECONDITION(p->is_nil());
 
   *p=tmp_what;
   return new_lhs;
@@ -172,9 +172,7 @@ void goto_symext::symex_assign_rec(
           lhs.id()==ID_complex_imag)
   {
     // this is stuff like __real__ x = 1;
-    DATA_INVARIANT(
-      lhs.operands().size() == 1,
-      "exprts with id ID_complex_real or ID_complex_imag take one operand.");
+    PRECONDITION(lhs.operands().size() == 1);
 
     exprt new_rhs=exprt(ID_complex, lhs.op0().type());
     new_rhs.operands().resize(2);
@@ -284,7 +282,6 @@ void goto_symext::symex_assign_typecast(
   assignment_typet assignment_type)
 {
   // these may come from dereferencing on the lhs
-
   PRECONDITION(lhs.operands().size() == 1);
 
   exprt rhs_typecasted=rhs;
@@ -307,7 +304,8 @@ void goto_symext::symex_assign_array(
   // lhs must be index operand
   // that takes two operands: the first must be an array
   // the second is the index
-  DATA_INVARIANT(lhs.operands().size() == 2, "index_exprt takes two operands");
+  DATA_INVARIANT(lhs.operands().size() == 2, 
+  	"index_exprt takes two operands: first must be array; second must be the index");
 
   const exprt &lhs_array=lhs.array();
   const exprt &lhs_index=lhs.index();
@@ -368,8 +366,7 @@ void goto_symext::symex_assign_struct_member(
   // typecasts involved? C++ does that for inheritance.
   if(lhs_struct.id()==ID_typecast)
   {
-    DATA_INVARIANT(
-      lhs_struct.operands().size() == 1, "typecast_exprt takes one operand.");
+    PRECONDITION(lhs_struct.operands().size() == 1);
 
     if(lhs_struct.op0().id() == ID_null_object)
     {
diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp
index c243cafbcd4..5559e0f5825 100644
--- a/src/goto-symex/symex_atomic_section.cpp
+++ b/src/goto-symex/symex_atomic_section.cpp
@@ -17,9 +17,9 @@ void goto_symext::symex_atomic_begin(statet &state)
     return;
 
   // we don't allow any nesting of atomic sections
-  if(state.atomic_section_id!=0)
-    throw "nested atomic section detected at "+
-      state.source.pc->source_location.as_string();
+  INVARIANT(state.atomic_section_id == 0, 
+  	"nested atomic section detected at " +
+      state.source.pc->source_location.as_string());
 
   state.atomic_section_id=++atomic_section_counter;
   state.read_in_atomic_section.clear();
@@ -36,8 +36,7 @@ void goto_symext::symex_atomic_end(statet &state)
   if(state.guard.is_false())
     return;
 
-  if(state.atomic_section_id==0)
-    throw "ATOMIC_END unmatched"; // NOLINT(readability/throw)
+  INVARIANT(state.atomic_section_id != 0, "ATOMIC_END unmatched");
 
   const unsigned atomic_section_id=state.atomic_section_id;
   state.atomic_section_id=0;
@@ -51,7 +50,7 @@ void goto_symext::symex_atomic_end(statet &state)
     r.set_level_2(r_it->second.first);
 
     // guard is the disjunction over reads
-    assert(!r_it->second.second.empty());
+    PRECONDITION(!r_it->second.second.empty());
     guardt read_guard(r_it->second.second.front());
     for(std::list<guardt>::const_iterator
         it=++(r_it->second.second.begin());
@@ -77,7 +76,7 @@ void goto_symext::symex_atomic_end(statet &state)
     w.set_level_2(state.level2.current_count(w.get_identifier()));
 
     // guard is the disjunction over writes
-    assert(!w_it->second.empty());
+    PRECONDITION(!w_it->second.empty());
     guardt write_guard(w_it->second.front());
     for(std::list<guardt>::const_iterator
         it=++(w_it->second.begin());
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 7b4be956854..5c345ae9b36 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -45,8 +45,7 @@ void goto_symext::symex_allocate(
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  if(code.operands().size()!=2)
-    throw "allocate expected to have two operands";
+  PRECONDITION(code.operands().size() == 2);
 
   if(lhs.is_nil())
     return; // ignore
@@ -162,8 +161,8 @@ void goto_symext::symex_allocate(
   state.rename(zero_init, ns); // to allow constant propagation
   simplify(zero_init, ns);
 
-  if(!zero_init.is_constant())
-    throw "allocate expects constant as second argument";
+  INVARIANT(zero_init.is_constant(),
+  	"allocate expects constant as second argument");
 
   if(!zero_init.is_zero() && !zero_init.is_false())
   {
@@ -175,13 +174,9 @@ void goto_symext::symex_allocate(
         ns,
         null_message);
 
-    if(zero_value.is_not_nil())
-    {
-      code_assignt assignment(value_symbol.symbol_expr(), zero_value);
-      symex_assign(state, assignment);
-    }
-    else
-      throw "failed to zero initialize dynamic object";
+    PRECONDITION(zero_value.is_not_nil())
+    code_assignt assignment(value_symbol.symbol_expr(), zero_value);
+    symex_assign(state, assignment);
   }
   else
   {
@@ -234,8 +229,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  if(code.operands().size()!=1)
-    throw "va_arg_next expected to have one operand";
+  PRECONDITION(code.operands().size() != 1);
 
   if(lhs.is_nil())
     return; // ignore
@@ -313,8 +307,7 @@ void goto_symext::symex_printf(
   statet &state,
   const exprt &rhs)
 {
-  if(rhs.operands().empty())
-    throw "printf expected to have at least one operand";
+  PRECONDITION(!rhs.operands().empty());
 
   exprt tmp_rhs=rhs;
   state.rename(tmp_rhs, ns);
@@ -339,8 +332,7 @@ void goto_symext::symex_input(
   statet &state,
   const codet &code)
 {
-  if(code.operands().size()<2)
-    throw "input expected to have at least two operands";
+  PRECONDITION(code.operands().size() >= 2);
 
   exprt id_arg=code.op0();
 
@@ -364,8 +356,7 @@ void goto_symext::symex_output(
   statet &state,
   const codet &code)
 {
-  if(code.operands().size()<2)
-    throw "output expected to have at least two operands";
+  PRECONDITION(code.operands().size() >= 2);
 
   exprt id_arg=code.op0();
 
@@ -397,8 +388,7 @@ void goto_symext::symex_cpp_new(
 {
   bool do_array;
 
-  if(code.type().id()!=ID_pointer)
-    throw "new expected to return pointer";
+  PRECONDITION(code.type().id() == ID_pointer);
 
   do_array =
     (code.get(ID_statement) == ID_cpp_new_array ||
@@ -466,9 +456,7 @@ void goto_symext::symex_trace(
   statet &state,
   const code_function_callt &code)
 {
-  if(code.arguments().size()<2)
-    // NOLINTNEXTLINE(readability/throw)
-    throw "symex_trace expects at least two arguments";
+  PRECONDITION(code.arguments().size() >= 2);
 
   int debug_thresh=unsafe_string2int(options.get_option("debug-level"));
 
@@ -530,37 +518,33 @@ void goto_symext::symex_macro(
 {
   const irep_idt &identifier=code.op0().get(ID_identifier);
 
-  if(identifier==CPROVER_MACRO_PREFIX "waitfor")
-  {
-    #if 0
-    exprt new_fc("waitfor", fc.type());
+  PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor")
+  #if 0
+  exprt new_fc("waitfor", fc.type());
 
-    if(fc.operands().size()!=4)
-      throw "waitfor expected to have four operands";
+  if(fc.operands().size()!=4)
+    throw "waitfor expected to have four operands";
 
-    exprt &cycle_var=fc.op1();
-    exprt &bound=fc.op2();
-    exprt &predicate=fc.op3();
+  exprt &cycle_var=fc.op1();
+  exprt &bound=fc.op2();
+  exprt &predicate=fc.op3();
 
-    if(cycle_var.id()!=ID_symbol)
-      throw "waitfor expects symbol as first operand but got "+
-            cycle_var.id();
+  if(cycle_var.id()!=ID_symbol)
+    throw "waitfor expects symbol as first operand but got "+
+          cycle_var.id();
 
-    exprt new_cycle_var(cycle_var);
-    new_cycle_var.id("waitfor_symbol");
-    new_cycle_var.copy_to_operands(bound);
+  exprt new_cycle_var(cycle_var);
+  new_cycle_var.id("waitfor_symbol");
+  new_cycle_var.copy_to_operands(bound);
 
-    replace_expr(cycle_var, new_cycle_var, predicate);
+  replace_expr(cycle_var, new_cycle_var, predicate);
 
-    new_fc.operands().resize(4);
-    new_fc.op0().swap(cycle_var);
-    new_fc.op1().swap(new_cycle_var);
-    new_fc.op2().swap(bound);
-    new_fc.op3().swap(predicate);
+  new_fc.operands().resize(4);
+  new_fc.op0().swap(cycle_var);
+  new_fc.op1().swap(new_cycle_var);
+  new_fc.op2().swap(bound);
+  new_fc.op3().swap(predicate);
 
-    fc.swap(new_fc);
-    #endif
-  }
-  else
-    throw "unknown macro: "+id2string(identifier);
+  fc.swap(new_fc);
+  #endif
 }
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index a6654c99409..d369885229d 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -23,12 +23,9 @@ void goto_symext::symex_dead(statet &state)
 
   const codet &code=to_code(instruction.code);
 
-  if(code.operands().size()!=1)
-    throw "dead expects one operand";
-
-  if(code.op0().id()!=ID_symbol)
-    throw "dead expects symbol as first operand";
-
+  PRECONDITION(code.operands().size()!=1);
+	PRECONDITION(code.op0().id()!=ID_symbol);
+  
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 776f8ddd2ed..94ba4f688d3 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -25,14 +25,11 @@ void goto_symext::symex_decl(statet &state)
 
   const codet &code=to_code(instruction.code);
 
-  if(code.operands().size()==2)
-    throw "two-operand decl not supported here";
-
-  if(code.operands().size()!=1)
-    throw "decl expects one operand";
-
-  if(code.op0().id()!=ID_symbol)
-    throw "decl expects symbol as first operand";
+  // two-operand decl not supported here
+  PRECONDITION(code.operands().size()!=2);
+  // we handle the decl with only one operand
+  PRECONDITION(code.operands().size()==1);
+  PRECONDITION(code.op0().id()!=ID_symbol);
 
   symex_decl(state, to_symbol_expr(code.op0()));
 }
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 26c8a5bccc4..4b0c60657e0 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -155,6 +155,7 @@ exprt goto_symext::address_arithmetic(
   }
   else if(expr.id()==ID_dereference)
   {
+  	PRECONDITION(expr.operands().size()==1);
     // ANSI-C guarantees &*p == p no matter what p is,
     // even if it's complete garbage
     // just grab the pointer, but be wary of further dereferencing
@@ -233,8 +234,7 @@ void goto_symext::dereference_rec(
 {
   if(expr.id()==ID_dereference)
   {
-    if(expr.operands().size()!=1)
-      throw "dereference takes one operand";
+    PRECONDITION(expr.operands().size()==1);
 
     bool expr_is_not_null = false;
 
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 1953e898a4c..abc778e1244 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -53,8 +53,7 @@ void goto_symext::parameter_assignments(
 
     const irep_idt &identifier=parameter.get_identifier();
 
-    if(identifier.empty())
-      throw "no identifier for function parameter";
+    INVARIANT(!identifier.empty(), "no identifier for function parameter");
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();
@@ -170,14 +169,11 @@ void goto_symext::symex_function_call(
 {
   const exprt &function=code.function();
 
-  if(function.id()==ID_symbol)
-    symex_function_call_symbol(get_goto_function, state, code);
-  else if(function.id()==ID_if)
-    throw "symex_function_call can't do if";
-  else if(function.id()==ID_dereference)
-    throw "symex_function_call can't do dereference";
-  else
-    throw "unexpected function for symex_function_call: "+function.id_string();
+  // If at some point symex_function_call can support more
+  // expression ids(), like ID_Dereference, please expand the
+  // precondition appropriately.
+  PRECONDITION(function.id() == ID_symbol);
+	symex_function_call_symbol(get_goto_function, state, code);
 }
 
 void goto_symext::symex_function_call_symbol(
@@ -431,28 +427,20 @@ void goto_symext::return_assignment(statet &state)
 
   target.location(state.guard.as_expr(), state.source);
 
-  if(code.operands().size()==1)
-  {
-    exprt value=code.op0();
+  PRECONDITION(code.operands().size() == 1);
+  
+  exprt value=code.op0();
 
-    if(frame.return_value.is_not_nil())
-    {
-      code_assignt assignment(frame.return_value, value);
+  if(frame.return_value.is_not_nil())
+  {
+    code_assignt assignment(frame.return_value, value);
 
-      if(!base_type_eq(assignment.lhs().type(),
-                       assignment.rhs().type(), ns))
-        throw
-          "goto_symext::return_assignment type mismatch at "+
-          instruction.source_location.as_string()+":\n"+
-          "assignment.lhs().type():\n"+assignment.lhs().type().pretty()+"\n"+
-          "assignment.rhs().type():\n"+assignment.rhs().type().pretty();
+    INVARIANT(
+    	base_type_eq(assignment.lhs().type(), assignment.rhs().type(), ns),
+      "goto_symext::return_assignment type mismatch");
 
-      symex_assign(state, assignment);
-    }
-  }
-  else
-  {
-    if(frame.return_value.is_not_nil())
-      throw "return with unexpected value";
+    symex_assign(state, assignment);
   }
+
+  POSTCONDITION(!frame.return_value.is_not_nil());
 }
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 0fed1309ce1..03b57e1be1b 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -48,8 +48,8 @@ void goto_symext::symex_goto(statet &state)
     !instruction.targets.empty(), "goto should have at least one target");
 
   // we only do deterministic gotos for now
-  if(instruction.targets.size()!=1)
-    throw "no support for non-deterministic gotos";
+  DATA_INVARIANT(
+  	instruction.targets.size()!=1, "no support for non-deterministic gotos");
 
   goto_programt::const_targett goto_target=
     instruction.get_target();
@@ -345,8 +345,7 @@ void goto_symext::merge_goto(
   statet &state)
 {
   // check atomic section
-  if(state.atomic_section_id!=goto_state.atomic_section_id)
-    throw "atomic sections differ across branches";
+  PRECONDITION(state.atomic_section_id == goto_state.atomic_section_id);
 
   // do SSA phi functions
   phi_function(goto_state, state);
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 63f1aa1d3b1..b80d20901d4 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -107,8 +107,8 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   {
     // forall X. P -> P
     // we keep the quantified variable unique by means of L2 renaming
-    PRECONDITION(expr.operands().size()==2);
-    PRECONDITION(expr.op0().id()==ID_symbol);
+    PRECONDITION(expr.operands().size() == 2);
+    PRECONDITION(expr.op0().id() == ID_symbol);
     symbol_exprt tmp0=
       to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
     symex_decl(state, tmp0);
@@ -464,6 +464,6 @@ void goto_symext::symex_step(
     throw "symex got NO_INSTRUCTION";
 
   default:
-    throw "symex got unexpected instruction";
+    UNREACHABLE;
   }
 }
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index c1ceff5c12d..7887161511d 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -137,9 +137,7 @@ void goto_symext::symex_other(
     // 3. build an assignment where the type on lhs and rhs is:
     // - array_copy: the type of the first array (even if the second is smaller)
     // - array_replace: the type of the second array (even if it is smaller)
-    DATA_INVARIANT(
-      code.operands().size() == 2,
-      "array_copy/array_replace takes two operands");
+  	PRECONDITION(code.operands().size() == 2);
 
     // we need to add dereferencing for both operands
     dereference_exprt dest_array(code.op0());
@@ -187,7 +185,7 @@ void goto_symext::symex_other(
     // process_array_expr)
     // 3. use the type of the resulting array to construct an array_of
     // expression
-    DATA_INVARIANT(code.operands().size() == 2, "array_set takes two operands");
+    PRECONDITION(code.operands().size() == 2);
 
     // we need to add dereferencing for the first operand
     exprt array_expr = dereference_exprt(code.op0());
@@ -232,9 +230,7 @@ void goto_symext::symex_other(
     // 3. build an assignment where the lhs is the previous third argument, and
     // the right-hand side is an equality over the arrays, if their types match;
     // if the types don't match the result trivially is false
-    DATA_INVARIANT(
-      code.operands().size() == 3,
-      "array_equal expected to take three arguments");
+    PRECONDITION(code.operands().size() == 3);
 
     // we need to add dereferencing for the first two
     dereference_exprt array1(code.op0());
@@ -266,8 +262,7 @@ void goto_symext::symex_other(
   }
   else if(statement==ID_havoc_object)
   {
-    DATA_INVARIANT(code.operands().size()==1,
-                   "havoc_object must have one operand");
+    PRECONDITION(code.operands().size()==1);
 
     // we need to add dereferencing for the first operand
     dereference_exprt object(code.op0(), empty_typet());
@@ -276,5 +271,5 @@ void goto_symext::symex_other(
     havoc_rec(state, guardt(), object);
   }
   else
-    throw "unexpected statement: "+id2string(statement);
+    UNREACHABLE;
 }
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 9986812598e..2dac55e56bd 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -20,16 +20,16 @@ void goto_symext::symex_start_thread(statet &state)
 
   // we don't allow spawning threads out of atomic sections
   // this would require amendments to ordering constraints
-  if(state.atomic_section_id!=0)
-    throw "start_thread in atomic section detected";
+  INVARIANT(state.atomic_section_id==0,
+    "start_thread in atomic section detected");
 
   // record this
   target.spawn(state.guard.as_expr(), state.source);
 
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  if(instruction.targets.size()!=1)
-    throw "start_thread expects one target";
+  INVARIANT(instruction.targets.size()==1,
+   "start_thread expects one target");
 
   goto_programt::const_targett thread_target=
     instruction.get_target();

From 112bd5bb90a57bb9ab8b0e100b48256b7b919979 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Mon, 23 Jul 2018 16:23:29 +0100
Subject: [PATCH 3/9] Add changes suggested during code review.

---
 src/goto-symex/build_goto_trace.cpp        |  2 +-
 src/goto-symex/goto_symex_state.cpp        |  5 +++--
 src/goto-symex/postcondition.cpp           | 17 ++++++++++++-----
 src/goto-symex/precondition.cpp            | 17 ++++++++++++-----
 src/goto-symex/slice_by_trace.cpp          |  4 ----
 src/goto-symex/symex_assign.cpp            | 20 +++++++++++++-------
 src/goto-symex/symex_atomic_section.cpp    |  7 +++----
 src/goto-symex/symex_builtin_functions.cpp |  6 +++---
 src/goto-symex/symex_dead.cpp              |  4 ++--
 src/goto-symex/symex_decl.cpp              |  1 -
 src/goto-symex/symex_dereference.cpp       |  8 ++++++--
 src/goto-symex/symex_function_call.cpp     |  8 ++++----
 src/goto-symex/symex_goto.cpp              |  2 +-
 src/goto-symex/symex_main.cpp              |  8 ++++++--
 src/goto-symex/symex_other.cpp             | 16 ++++++++++++----
 15 files changed, 78 insertions(+), 47 deletions(-)

diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 1a20a5266e0..7997cbce7ec 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -222,7 +222,7 @@ void build_goto_trace(
       else if(it->is_atomic_end() && current_time<0)
         current_time*=-1;
 
-      PRECONDITION(current_time>=0);
+      INVARIANT(current_time>=0, "time keeping inconsistency");
       // move any steps gathered in an atomic section
 
       if(time_before<0)
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 0af0547490b..fe5625f218e 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -493,9 +493,10 @@ void goto_symex_statet::rename(
   }
   else if(expr.id()==ID_address_of)
   {
-    PRECONDITION(expr.operands().size() == 1);
-    rename_address(expr.op0(), ns, level);
     PRECONDITION(expr.type().id() == ID_pointer);
+    DATA_INVARIANT(
+    	expr.operands().size() == 1, "address_of should have a single operand");
+    rename_address(expr.op0(), ns, level);
     expr.type().subtype()=expr.op0().type();
   }
   else
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 462417871e8..62472711773 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -76,19 +76,22 @@ bool postconditiont::is_used_address_of(
   }
   else if(expr.id()==ID_index)
   {
-    PRECONDITION(expr.operands().size() == 2);
+    DATA_INVARIANT(
+    	expr.operands().size() == 2, "index expression should have two operands");
     return
       is_used_address_of(expr.op0(), identifier) ||
       is_used(expr.op1(), identifier);
   }
   else if(expr.id()==ID_member)
   {
-    PRECONDITION(expr.operands().size() == 1);
+    DATA_INVARIANT(
+    	expr.operands().size() == 1, "member expression should only have one operand");
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_dereference)
   {
-    PRECONDITION(expr.operands().size() == 1);
+    DATA_INVARIANT(
+    	expr.operands().size() == 1, "dereference expression should only have one operand");
     return is_used(expr.op0(), identifier);
   }
 
@@ -154,7 +157,9 @@ bool postconditiont::is_used(
   if(expr.id()==ID_address_of)
   {
     // only do index!
-    PRECONDITION(expr.operands().size() == 1);
+    DATA_INVARIANT(
+    	expr.operands().size() == 1,
+    	"address_of expression expected to have one operand at this point");
     return is_used_address_of(expr.op0(), identifier);
   }
   else if(expr.id()==ID_symbol &&
@@ -168,7 +173,9 @@ bool postconditiont::is_used(
   }
   else if(expr.id()==ID_dereference)
   {
-    PRECONDITION(expr.operands().size() == 1);
+    DATA_INVARIANT(
+    	expr.operands().size() == 1,
+    	"dereference expression expected to have one operand");
 
     // aliasing may happen here
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 111d3e339f5..67fdbae9640 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -78,18 +78,21 @@ void preconditiont::compute_address_of(exprt &dest)
   }
   else if(dest.id()==ID_index)
   {
-    PRECONDITION(dest.operands().size() == 2);
+    DATA_INVARIANT(
+    	dest.operands().size() == 2, "index expression expected to have two operands");
     compute_address_of(dest.op0());
     compute(dest.op1());
   }
   else if(dest.id()==ID_member)
   {
-    PRECONDITION(dest.operands().size() == 1);
+    DATA_INVARIANT(
+    	dest.operands().size() == 1, "member expression expected to have one operand");
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
-    PRECONDITION(dest.operands().size() == 1);
+    DATA_INVARIANT(
+    	dest.operands().size() == 1, "dereference expression expected to have 1 operand");
     compute(dest.op0());
   }
 }
@@ -104,12 +107,16 @@ void preconditiont::compute_rec(exprt &dest)
   if(dest.id()==ID_address_of)
   {
     // only do index!
-    PRECONDITION(dest.operands().size() == 1);
+    DATA_INVARIANT(
+    	dest.operands().size() == 1,
+    	"address_of expression expected to have one operand at this point");
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
-    PRECONDITION(dest.operands().size() == 1);
+    DATA_INVARIANT(
+    	dest.operands().size() == 1,
+    	"dereference expression expected to have one operand at this point");
 
     const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
 
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index 36056617674..0b84e49bfd5 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -99,10 +99,6 @@ void symex_slice_by_tracet::slice_by_trace(
       simplify(copy_last, ns);
       implications.insert(copy_last);
     }
-    else if(!(g_copy.id()==ID_constant))
-    {
-      UNHANDLED_CASE;
-    }
   }
 
   slice_SSA_steps(equation, implications); // Slice based on implications
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 5292e0492d4..98b775a4d4e 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -55,8 +55,9 @@ void goto_symext::symex_assign(
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
     {
-      if(lhs.is_not_nil())
-        throw "printf: unexpected assignment";
+    	PRECONDITION(!lhs.is_not_nil());
+      // if(lhs.is_not_nil())
+        // throw "printf: unexpected assignment";
       symex_printf(state, side_effect_expr);
     }
     else if(statement==ID_gcc_builtin_va_arg_next)
@@ -106,12 +107,15 @@ exprt goto_symext::add_to_lhs(
 
   while(p->is_not_nil())
   {
-    PRECONDITION(p->id()!=ID_symbol);
-    PRECONDITION(p->operands().size()>=1);
+    INVARIANT(
+    	p->id() != ID_symbol, "expected pointed-to expression to be a symbol");
+    INVARIANT(
+    	p->operands().size() >= 1,
+    	"expected pointed-to expression to have at least one operand");
     p=&p->op0();
   }
 
-  PRECONDITION(p->is_nil());
+  INVARIANT(p->is_nil(), "expected pointed-to expression to be nil at this point");
 
   *p=tmp_what;
   return new_lhs;
@@ -366,7 +370,9 @@ void goto_symext::symex_assign_struct_member(
   // typecasts involved? C++ does that for inheritance.
   if(lhs_struct.id()==ID_typecast)
   {
-    PRECONDITION(lhs_struct.operands().size() == 1);
+    DATA_INVARIANT(
+    	lhs_struct.operands().size() == 1,
+    	"typecast expression expected to have one operand");
 
     if(lhs_struct.op0().id() == ID_null_object)
     {
@@ -445,7 +451,7 @@ void goto_symext::symex_assign_if(
     guard.swap(old_guard);
   }
 
-  if(!renamed_guard.is_true())
+if(!renamed_guard.is_true())
   {
     guard.add(not_exprt(renamed_guard));
     symex_assign_rec(
diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp
index 5559e0f5825..7f38af2ee1e 100644
--- a/src/goto-symex/symex_atomic_section.cpp
+++ b/src/goto-symex/symex_atomic_section.cpp
@@ -16,10 +16,9 @@ void goto_symext::symex_atomic_begin(statet &state)
   if(state.guard.is_false())
     return;
 
-  // we don't allow any nesting of atomic sections
-  INVARIANT(state.atomic_section_id == 0, 
-  	"nested atomic section detected at " +
-      state.source.pc->source_location.as_string());
+  INVARIANT(
+  	state.atomic_section_id == 0, 
+  	"we don't support nesting of atomic sections");
 
   state.atomic_section_id=++atomic_section_counter;
   state.read_in_atomic_section.clear();
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 5c345ae9b36..a9bb4f7be3e 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -174,7 +174,7 @@ void goto_symext::symex_allocate(
         ns,
         null_message);
 
-    PRECONDITION(zero_value.is_not_nil())
+    CHECK_RETURN(zero_value.is_not_nil());
     code_assignt assignment(value_symbol.symbol_expr(), zero_value);
     symex_assign(state, assignment);
   }
@@ -229,7 +229,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  PRECONDITION(code.operands().size() != 1);
+  PRECONDITION(code.operands().size() == 1);
 
   if(lhs.is_nil())
     return; // ignore
@@ -518,7 +518,7 @@ void goto_symext::symex_macro(
 {
   const irep_idt &identifier=code.op0().get(ID_identifier);
 
-  PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor")
+  PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor");
   #if 0
   exprt new_fc("waitfor", fc.type());
 
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index d369885229d..c94e1d3dc7d 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -23,8 +23,8 @@ void goto_symext::symex_dead(statet &state)
 
   const codet &code=to_code(instruction.code);
 
-  PRECONDITION(code.operands().size()!=1);
-	PRECONDITION(code.op0().id()!=ID_symbol);
+  PRECONDITION(code.operands().size()==1);
+  PRECONDITION(code.op0().id()==ID_symbol);
   
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 94ba4f688d3..b51b5a70bf2 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -26,7 +26,6 @@ void goto_symext::symex_decl(statet &state)
   const codet &code=to_code(instruction.code);
 
   // two-operand decl not supported here
-  PRECONDITION(code.operands().size()!=2);
   // we handle the decl with only one operand
   PRECONDITION(code.operands().size()==1);
   PRECONDITION(code.op0().id()!=ID_symbol);
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 4b0c60657e0..bc60f21a01a 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -155,7 +155,9 @@ exprt goto_symext::address_arithmetic(
   }
   else if(expr.id()==ID_dereference)
   {
-  	PRECONDITION(expr.operands().size()==1);
+  	DATA_INVARIANT(
+  		expr.operands().size() == 1,
+  		"dereference expression expected to have one operand");
     // ANSI-C guarantees &*p == p no matter what p is,
     // even if it's complete garbage
     // just grab the pointer, but be wary of further dereferencing
@@ -234,7 +236,9 @@ void goto_symext::dereference_rec(
 {
   if(expr.id()==ID_dereference)
   {
-    PRECONDITION(expr.operands().size()==1);
+    DATA_INVARIANT(
+    	expr.operands().size() == 1,
+    	"dereference expression expected to have one operand");
 
     bool expr_is_not_null = false;
 
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index abc778e1244..027838ad0e6 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -173,7 +173,7 @@ void goto_symext::symex_function_call(
   // expression ids(), like ID_Dereference, please expand the
   // precondition appropriately.
   PRECONDITION(function.id() == ID_symbol);
-	symex_function_call_symbol(get_goto_function, state, code);
+  symex_function_call_symbol(get_goto_function, state, code);
 }
 
 void goto_symext::symex_function_call_symbol(
@@ -427,7 +427,9 @@ void goto_symext::return_assignment(statet &state)
 
   target.location(state.guard.as_expr(), state.source);
 
-  PRECONDITION(code.operands().size() == 1);
+  PRECONDITION(
+  	code.operands().size() == 1 ||
+  	frame.return_value.is_nil());
   
   exprt value=code.op0();
 
@@ -441,6 +443,4 @@ void goto_symext::return_assignment(statet &state)
 
     symex_assign(state, assignment);
   }
-
-  POSTCONDITION(!frame.return_value.is_not_nil());
 }
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 03b57e1be1b..e4e0ddd28e4 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -49,7 +49,7 @@ void goto_symext::symex_goto(statet &state)
 
   // we only do deterministic gotos for now
   DATA_INVARIANT(
-  	instruction.targets.size()!=1, "no support for non-deterministic gotos");
+  	instruction.targets.size() == 1, "no support for non-deterministic gotos");
 
   goto_programt::const_targett goto_target=
     instruction.get_target();
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index b80d20901d4..1f645f3f3e2 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -107,8 +107,12 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   {
     // forall X. P -> P
     // we keep the quantified variable unique by means of L2 renaming
-    PRECONDITION(expr.operands().size() == 2);
-    PRECONDITION(expr.op0().id() == ID_symbol);
+    DATA_INVARIANT(
+    	expr.operands().size() == 2,
+    	"for_all expression expected to have two operands");
+    DATA_INVARIANT(
+    	expr.op0().id() == ID_symbol,
+    	"first operand of for_all expression expected to be a symbol");
     symbol_exprt tmp0=
       to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
     symex_decl(state, tmp0);
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 7887161511d..a2361e4e23e 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -137,7 +137,9 @@ void goto_symext::symex_other(
     // 3. build an assignment where the type on lhs and rhs is:
     // - array_copy: the type of the first array (even if the second is smaller)
     // - array_replace: the type of the second array (even if it is smaller)
-  	PRECONDITION(code.operands().size() == 2);
+  	DATA_INVARIANT(
+  		code.operands().size() == 2,
+  		"expected statement to have two operands at this point");
 
     // we need to add dereferencing for both operands
     dereference_exprt dest_array(code.op0());
@@ -185,7 +187,9 @@ void goto_symext::symex_other(
     // process_array_expr)
     // 3. use the type of the resulting array to construct an array_of
     // expression
-    PRECONDITION(code.operands().size() == 2);
+    DATA_INVARIANT(
+  		code.operands().size() == 2,
+  		"expected statement to have two operands at this point");
 
     // we need to add dereferencing for the first operand
     exprt array_expr = dereference_exprt(code.op0());
@@ -230,7 +234,9 @@ void goto_symext::symex_other(
     // 3. build an assignment where the lhs is the previous third argument, and
     // the right-hand side is an equality over the arrays, if their types match;
     // if the types don't match the result trivially is false
-    PRECONDITION(code.operands().size() == 3);
+    DATA_INVARIANT(
+  		code.operands().size() == 3,
+  		"expected statement to have three operands at this point");
 
     // we need to add dereferencing for the first two
     dereference_exprt array1(code.op0());
@@ -262,7 +268,9 @@ void goto_symext::symex_other(
   }
   else if(statement==ID_havoc_object)
   {
-    PRECONDITION(code.operands().size()==1);
+    DATA_INVARIANT(
+  		code.operands().size() == 1,
+  		"expected statement to have one operand at this point");
 
     // we need to add dereferencing for the first operand
     dereference_exprt object(code.op0(), empty_typet());

From c7fb551dfe10f222f3953fe61b5a84b7b78edb3c Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Tue, 24 Jul 2018 10:12:09 +0100
Subject: [PATCH 4/9] Move equation conversion exception to exception utils

---
 .../equation_conversion_exceptions.h          | 47 -------------------
 src/goto-symex/symex_target_equation.cpp      |  2 +-
 src/util/exception_utils.h                    | 32 +++++++++++++
 3 files changed, 33 insertions(+), 48 deletions(-)
 delete mode 100644 src/goto-symex/equation_conversion_exceptions.h

diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h
deleted file mode 100644
index ffa57abefe0..00000000000
--- a/src/goto-symex/equation_conversion_exceptions.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*******************************************************************\
-
-Module: Symbolic Execution
-
-Author: Diffblue Ltd.
-
-\*******************************************************************/
-
-/// \file
-/// Exceptions that can be raised during the equation conversion phase
-
-#ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
-#define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
-
-#include <sstream>
-
-#include <util/format_expr.h>
-
-#include "symex_target_equation.h"
-
-class equation_conversion_exceptiont : public std::runtime_error
-{
-public:
-  equation_conversion_exceptiont(
-    const std::string &message,
-    const symex_target_equationt::SSA_stept &step)
-    : runtime_error(message), step(step)
-  {
-    std::ostringstream error_msg;
-    error_msg << runtime_error::what();
-    error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
-    error_msg << "\nStep:\n";
-    step.output(error_msg);
-    error_message = error_msg.str();
-  }
-
-  const char *what() const optional_noexcept override
-  {
-    return error_message.c_str();
-  }
-
-private:
-  symex_target_equationt::SSA_stept step;
-  std::string error_message;
-};
-
-#endif // CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 1f906f3f8d7..0c90f84928f 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
 #include <util/unwrap_nested_exception.h>
+#include <util/exception_utils.h>
 
 // Can be removed once deprecated SSA_stept::output is removed
 #include <langapi/language_util.h>
@@ -24,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
 
-#include "equation_conversion_exceptions.h"
 #include "goto_symex_state.h"
 
 /// read from a shared variable
diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h
index 73938fe1826..5d162b3c971 100644
--- a/src/util/exception_utils.h
+++ b/src/util/exception_utils.h
@@ -10,6 +10,11 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com
 #define CPROVER_UTIL_EXCEPTION_UTILS_H
 
 #include <string>
+#include <sstream>
+
+#include <goto-symex/symex_target_equation.h>
+
+#include "format_expr.h"
 
 class invalid_user_input_exceptiont
 {
@@ -38,4 +43,31 @@ class invalid_user_input_exceptiont
   }
 };
 
+
+class equation_conversion_exceptiont : public std::runtime_error
+{
+public:
+  equation_conversion_exceptiont(
+    const std::string &message,
+    const symex_target_equationt::SSA_stept &step)
+    : runtime_error(message), step(step)
+  {
+    std::ostringstream error_msg;
+    error_msg << runtime_error::what();
+    error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
+    error_msg << "\nStep:\n";
+    step.output(error_msg);
+    error_message = error_msg.str();
+  }
+
+  const char *what() const optional_noexcept override
+  {
+    return error_message.c_str();
+  }
+
+private:
+  symex_target_equationt::SSA_stept step;
+  std::string error_message;
+};
+
 #endif // CPROVER_UTIL_EXCEPTION_UTILS_H

From b43902e9a61f7e42aada186f6abeb34d5b1f3c42 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Fri, 27 Jul 2018 10:02:54 +0100
Subject: [PATCH 5/9] Address the latest review comments.

---
 src/goto-symex/build_goto_trace.cpp          |  4 +++-
 src/goto-symex/goto_symex_state.cpp          | 11 ++++++++---
 src/goto-symex/partial_order_concurrency.cpp |  2 +-
 src/goto-symex/slice_by_trace.cpp            |  2 +-
 src/goto-symex/symex_assign.cpp              | 10 +++++-----
 src/goto-symex/symex_decl.cpp                |  4 ++--
 src/goto-symex/symex_function_call.cpp       |  3 ++-
 src/goto-symex/symex_goto.cpp                |  4 +++-
 src/goto-symex/symex_other.cpp               |  8 ++++----
 9 files changed, 29 insertions(+), 19 deletions(-)

diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 7997cbce7ec..7e3207d377d 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -91,8 +91,10 @@ exprt build_full_lhs_rec(
   else if(id==ID_byte_extract_little_endian ||
           id==ID_byte_extract_big_endian)
   {
+  	DATA_INVARIANT(
+    	src_original.operands().size() == 2,
+    	"byte extract expressions require two operands");
     exprt tmp=src_original;
-    PRECONDITION(tmp.operands().size() == 2);
     tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
 
     // re-write into big case-split
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index fe5625f218e..52ba7e9e2ba 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -186,7 +186,9 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   }
   else if(expr.id()==ID_member)
   {
-    PRECONDITION(expr.operands().size() == 1);
+    DATA_INVARIANT(
+    	expr.operands().size() == 1,
+    	"member expression expects one operand");
 
     return constant_propagation_reference(expr.op0());
   }
@@ -493,9 +495,12 @@ void goto_symex_statet::rename(
   }
   else if(expr.id()==ID_address_of)
   {
-    PRECONDITION(expr.type().id() == ID_pointer);
     DATA_INVARIANT(
-    	expr.operands().size() == 1, "address_of should have a single operand");
+    	expr.type().id() == ID_pointer,
+    	"type of expression required to be pointer");
+    DATA_INVARIANT(
+    	expr.operands().size() == 1,
+    	"address_of should have a single operand");
     rename_address(expr.op0(), ns, level);
     expr.type().subtype()=expr.op0().type();
   }
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index 49204e1c678..2984e847e5f 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -142,8 +142,8 @@ symbol_exprt partial_order_concurrencyt::clock(
   event_it event,
   axiomt axiom)
 {
+	PRECONDITION(!numbering.empty());
   irep_idt identifier;
-  PRECONDITION(!numbering.empty());
 
   if(event->is_shared_write())
     identifier=rw_clock_id(event, axiom);
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index 0b84e49bfd5..535cf3d47b8 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -79,7 +79,7 @@ void symex_slice_by_tracet::slice_by_trace(
   {
     exprt g_copy(*i);
 
-    INVARIANT(
+    DATA_INVARIANT(
     	g_copy.id() == ID_symbol || 
     	g_copy.id() == ID_not ||
     	g_copy.id() == ID_and ||
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 98b775a4d4e..59e2e296b70 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -37,7 +37,9 @@ void goto_symext::symex_assign(
 
     if(statement==ID_function_call)
     {
-      PRECONDITION(!side_effect_expr.operands().empty());
+      DATA_INVARIANT(
+      	!side_effect_expr.operands().empty()
+      	"function call stamement expects non-empty list of side effects");
 
       if(side_effect_expr.op0().id()!=ID_symbol)
         throw "symex_assign: expected symbol as function";
@@ -55,9 +57,7 @@ void goto_symext::symex_assign(
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
     {
-    	PRECONDITION(!lhs.is_not_nil());
-      // if(lhs.is_not_nil())
-        // throw "printf: unexpected assignment";
+    	PRECONDITION(lhs.is_nil());
       symex_printf(state, side_effect_expr);
     }
     else if(statement==ID_gcc_builtin_va_arg_next)
@@ -115,7 +115,7 @@ exprt goto_symext::add_to_lhs(
     p=&p->op0();
   }
 
-  INVARIANT(p->is_nil(), "expected pointed-to expression to be nil at this point");
+  INVARIANT(p->is_nil(), "expected pointed-to expression to be nil");
 
   *p=tmp_what;
   return new_lhs;
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index b51b5a70bf2..45f80595db7 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -27,8 +27,8 @@ void goto_symext::symex_decl(statet &state)
 
   // two-operand decl not supported here
   // we handle the decl with only one operand
-  PRECONDITION(code.operands().size()==1);
-  PRECONDITION(code.op0().id()!=ID_symbol);
+  PRECONDITION(code.operands().size() == 1);
+  PRECONDITION(code.op0().id() == ID_symbol);
 
   symex_decl(state, to_symbol_expr(code.op0()));
 }
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 027838ad0e6..222f09a1f53 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -53,7 +53,8 @@ void goto_symext::parameter_assignments(
 
     const irep_idt &identifier=parameter.get_identifier();
 
-    INVARIANT(!identifier.empty(), "no identifier for function parameter");
+    INVARIANT(!identifier.empty(), 
+    	"function pointer parameter must have an identifier");
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index e4e0ddd28e4..eddff0c040b 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -345,7 +345,9 @@ void goto_symext::merge_goto(
   statet &state)
 {
   // check atomic section
-  PRECONDITION(state.atomic_section_id == goto_state.atomic_section_id);
+  INVARIANT(
+  	state.atomic_section_id == goto_state.atomic_section_id,
+  	"atomic sections differ across branches");
 
   // do SSA phi functions
   phi_function(goto_state, state);
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index a2361e4e23e..68e0bf97f1e 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -139,7 +139,7 @@ void goto_symext::symex_other(
     // - array_replace: the type of the second array (even if it is smaller)
   	DATA_INVARIANT(
   		code.operands().size() == 2,
-  		"expected statement to have two operands at this point");
+  		"expected array copy/array replace statement to have two operands");
 
     // we need to add dereferencing for both operands
     dereference_exprt dest_array(code.op0());
@@ -189,7 +189,7 @@ void goto_symext::symex_other(
     // expression
     DATA_INVARIANT(
   		code.operands().size() == 2,
-  		"expected statement to have two operands at this point");
+  		"expected array_set statement to have two operands");
 
     // we need to add dereferencing for the first operand
     exprt array_expr = dereference_exprt(code.op0());
@@ -236,7 +236,7 @@ void goto_symext::symex_other(
     // if the types don't match the result trivially is false
     DATA_INVARIANT(
   		code.operands().size() == 3,
-  		"expected statement to have three operands at this point");
+  		"expected array_equal statement to have three operands");
 
     // we need to add dereferencing for the first two
     dereference_exprt array1(code.op0());
@@ -270,7 +270,7 @@ void goto_symext::symex_other(
   {
     DATA_INVARIANT(
   		code.operands().size() == 1,
-  		"expected statement to have one operand at this point");
+  		"expected havoc_object statement to have one operand");
 
     // we need to add dereferencing for the first operand
     dereference_exprt object(code.op0(), empty_typet());

From 2d913c46c1c2fd2ae2e438272b477f5d4ae730aa Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 30 Aug 2018 11:52:43 +0100
Subject: [PATCH 6/9] Fixup into second

---
 src/goto-symex/symex_dereference.cpp | 6 +++---
 src/goto-symex/symex_other.cpp       | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index bc60f21a01a..bc313d63487 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -155,9 +155,9 @@ exprt goto_symext::address_arithmetic(
   }
   else if(expr.id()==ID_dereference)
   {
-  	DATA_INVARIANT(
-  		expr.operands().size() == 1,
-  		"dereference expression expected to have one operand");
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      "dereference expression expected to have one operand");
     // ANSI-C guarantees &*p == p no matter what p is,
     // even if it's complete garbage
     // just grab the pointer, but be wary of further dereferencing
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 68e0bf97f1e..49642d1e78b 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -139,7 +139,7 @@ void goto_symext::symex_other(
     // - array_replace: the type of the second array (even if it is smaller)
   	DATA_INVARIANT(
   		code.operands().size() == 2,
-  		"expected array copy/array replace statement to have two operands");
+  		"expected array_copy/array_replace statement to have two operands");
 
     // we need to add dereferencing for both operands
     dereference_exprt dest_array(code.op0());

From 77b43ea8d37dd6c20d58f528251d042e1aa614b5 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 30 Aug 2018 11:55:58 +0100
Subject: [PATCH 7/9] Add into the third one.

---
 src/goto-symex/symex_other.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 49642d1e78b..84c1fd756e1 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -137,9 +137,9 @@ void goto_symext::symex_other(
     // 3. build an assignment where the type on lhs and rhs is:
     // - array_copy: the type of the first array (even if the second is smaller)
     // - array_replace: the type of the second array (even if it is smaller)
-  	DATA_INVARIANT(
-  		code.operands().size() == 2,
-  		"expected array_copy/array_replace statement to have two operands");
+    DATA_INVARIANT(
+      code.operands().size() == 2,
+      "expected array_copy/array_replace statement to have two operands");
 
     // we need to add dereferencing for both operands
     dereference_exprt dest_array(code.op0());

From 46aeea42de8f38d7168170068d22b0c704ede4fb Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 30 Aug 2018 16:30:11 +0100
Subject: [PATCH 8/9] Some minor fixes

---
 src/goto-symex/symex_assign.cpp       | 2 +-
 src/goto-symex/symex_start_thread.cpp | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 59e2e296b70..71ad7dc049b 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -38,7 +38,7 @@ void goto_symext::symex_assign(
     if(statement==ID_function_call)
     {
       DATA_INVARIANT(
-      	!side_effect_expr.operands().empty()
+      	!side_effect_expr.operands().empty(),
       	"function call stamement expects non-empty list of side effects");
 
       if(side_effect_expr.op0().id()!=ID_symbol)
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 2dac55e56bd..b26132ba514 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -18,10 +18,9 @@ void goto_symext::symex_start_thread(statet &state)
   if(state.guard.is_false())
     return;
 
-  // we don't allow spawning threads out of atomic sections
-  // this would require amendments to ordering constraints
-  INVARIANT(state.atomic_section_id==0,
-    "start_thread in atomic section detected");
+  INVARIANT(state.atomic_section_id == 0,
+    "spawning threads out of atomic sections is not allowed; "
+    "this would require amendments to ordering constraints");
 
   // record this
   target.spawn(state.guard.as_expr(), state.source);

From f2a7a37dcc699c73bb2c8fd835342f4589f7b9ab Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Fri, 31 Aug 2018 15:33:31 +0100
Subject: [PATCH 9/9] Some more changes.

---
 src/goto-symex/symex_assign.cpp       | 17 ++++++++---------
 src/goto-symex/symex_start_thread.cpp |  2 +-
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 71ad7dc049b..72a307638ab 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -41,8 +41,9 @@ void goto_symext::symex_assign(
       	!side_effect_expr.operands().empty(),
       	"function call stamement expects non-empty list of side effects");
 
-      if(side_effect_expr.op0().id()!=ID_symbol)
-        throw "symex_assign: expected symbol as function";
+      DATA_INVARIANT(
+      	side_effect_expr.op0().id() == ID_symbol,
+        "expected symbol as function");
 
       const irep_idt &identifier=
         to_symbol_expr(side_effect_expr.op0()).get_identifier();
@@ -63,7 +64,7 @@ void goto_symext::symex_assign(
     else if(statement==ID_gcc_builtin_va_arg_next)
       symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
     else
-      throw "symex_assign: unexpected side effect: "+id2string(statement);
+      UNREACHABLE;
   }
   else
   {
@@ -313,11 +314,9 @@ void goto_symext::symex_assign_array(
 
   const exprt &lhs_array=lhs.array();
   const exprt &lhs_index=lhs.index();
-  const typet &lhs_type=ns.follow(lhs_array.type());
+  const typet &lhs_index_type=ns.follow(lhs_array.type());
 
-  if(lhs_type.id()!=ID_array)
-    throw "index must take array type operand, but got `"+
-          lhs_type.id_string()+"'";
+  PRECONDITION(lhs_index_type.id() == ID_array);
 
   #ifdef USE_UPDATE
 
@@ -326,7 +325,7 @@ void goto_symext::symex_assign_array(
   // into
   //   a'==UPDATE(a, [i], e)
 
-  update_exprt new_rhs(lhs_type);
+  update_exprt new_rhs(lhs_index_type);
   new_rhs.old()=lhs_array;
   new_rhs.designator().push_back(index_designatort(lhs_index));
   new_rhs.new_value()=rhs;
@@ -343,7 +342,7 @@ void goto_symext::symex_assign_array(
   //   a'==a WITH [i:=e]
 
   with_exprt new_rhs(lhs_array, lhs_index, rhs);
-  new_rhs.type() = lhs_type;
+  new_rhs.type() = lhs_index_type;
 
   exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
 
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index b26132ba514..9edf253c195 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -27,7 +27,7 @@ void goto_symext::symex_start_thread(statet &state)
 
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  INVARIANT(instruction.targets.size()==1,
+  INVARIANT(instruction.targets.size() == 1,
    "start_thread expects one target");
 
   goto_programt::const_targett thread_target=