diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 185b6c8b858..a6502391c3e 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -11,7 +11,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
-#include <cstdlib>
+#ifdef DEBUG
+#include <iostream>
+#endif
 
 #include <util/pointer_offset_size.h>
 #include <util/std_types.h>
@@ -20,6 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/config.h>
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
+#include <util/invariant.h>
 
 #include <util/c_types.h>
 #include <ansi-c/c_qualifiers.h>
@@ -69,25 +72,27 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr)
     typecheck_expr_explicit_constructor_call(expr);
   else if(expr.is_nil())
   {
-    #if 0
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got nil\n";
-    #endif
-    abort();
+#endif
+    UNREACHABLE;
   }
   else if(expr.id()==ID_code)
   {
-    #if 0
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got code\n";
-    #endif
-    abort();
+#endif
+    UNREACHABLE;
   }
   else if(expr.id()==ID_symbol)
   {
-    #if 0
-    std::cout << "E: " << expr.pretty() << '\n';
+    // ignore here
+#ifdef DEBUG
+    std::cerr << "E: " << expr.pretty() << '\n';
     std::cerr << "cpp_typecheckt::typecheck_expr_main got symbol\n";
-    abort();
-    #endif
+#endif
   }
   else if(expr.id()=="__is_base_of")
   {
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index f1c1e325e46..23f7fea3f0b 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -50,12 +50,9 @@ void goto_symex_statet::level0t::operator()(
     return;
 
   const symbolt *s;
-
-  if(ns.lookup(obj_identifier, s))
-  {
-    std::cerr << "level0: failed to find " << obj_identifier << '\n';
-    abort();
-  }
+  const bool found_l0 = !ns.lookup(obj_identifier, s);
+  DATA_INVARIANT(
+    found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id()==ID_code ||
diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp
index 0486874d6d2..fc4e66935d9 100644
--- a/src/solvers/flattening/boolbv_add_sub.cpp
+++ b/src/solvers/flattening/boolbv_add_sub.cpp
@@ -8,8 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-#include <iostream>
-
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 #include "../floatbv/float_utils.h"
@@ -38,12 +37,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
     throw "operator "+expr.id_string()+" takes at least one operand";
 
   const exprt &op0=expr.op0();
-
-  if(op0.type()!=type)
-  {
-    std::cerr << expr.pretty() << '\n';
-    throw "add/sub with mixed types";
-  }
+  DATA_INVARIANT(
+    op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
   bvt bv=convert_bv(op0);
 
@@ -69,11 +64,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
       it=operands.begin()+1;
       it!=operands.end(); it++)
   {
-    if(it->type()!=type)
-    {
-      std::cerr << expr.pretty() << '\n';
-      throw "add/sub with mixed types";
-    }
+    DATA_INVARIANT(
+      it->type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
     const bvt &op=convert_bv(*it);
 
diff --git a/src/solvers/flattening/boolbv_case.cpp b/src/solvers/flattening/boolbv_case.cpp
index 6434f216178..7e1d2280a32 100644
--- a/src/solvers/flattening/boolbv_case.cpp
+++ b/src/solvers/flattening/boolbv_case.cpp
@@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-#include <iostream>
+#include <util/invariant.h>
 
 bvt boolbvt::convert_case(const exprt &expr)
 {
@@ -49,15 +49,11 @@ bvt boolbvt::convert_case(const exprt &expr)
       break;
 
     case COMPARE:
-      if(compare_bv.size()!=op.size())
-      {
-        std::cerr << "compare operand: " << compare_bv.size()
-                  << "\noperand: " << op.size() << '\n'
-                  << it->pretty()
-                  << '\n';
-
-        throw "size of compare operand does not match";
-      }
+      DATA_INVARIANT(
+        compare_bv.size() == op.size(),
+        std::string("size of compare operand does not match:\n") +
+          "compare operand: " + std::to_string(compare_bv.size()) +
+          "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
 
       compare_literal=bv_utils.equal(compare_bv, op);
       compare_literal=prop.land(!previous_compare, compare_literal);
@@ -68,15 +64,11 @@ bvt boolbvt::convert_case(const exprt &expr)
       break;
 
     case VALUE:
-      if(bv.size()!=op.size())
-      {
-        std::cerr << "result size: " << bv.size()
-                  << "\noperand: " << op.size() << '\n'
-                  << it->pretty()
-                  << '\n';
-
-        throw "size of value operand does not match";
-      }
+      DATA_INVARIANT(
+        bv.size() == op.size(),
+        std::string("size of value operand does not match:\n") +
+          "result size: " + std::to_string(bv.size()) +
+          "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
 
       {
         literalt value_literal=bv_utils.equal(bv, op);
diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp
index 514c1e817f3..e6bb129b0d4 100644
--- a/src/solvers/flattening/boolbv_cond.cpp
+++ b/src/solvers/flattening/boolbv_cond.cpp
@@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-#include <iostream>
+#include <util/invariant.h>
 
 bvt boolbvt::convert_cond(const exprt &expr)
 {
@@ -51,15 +51,11 @@ bvt boolbvt::convert_cond(const exprt &expr)
       {
         const bvt &op=convert_bv(*it);
 
-        if(bv.size()!=op.size())
-        {
-          std::cerr << "result size: " << bv.size()
-                    << "\noperand: " << op.size() << '\n'
-                    << it->pretty()
-                    << '\n';
-
-          throw "size of value operand does not match";
-        }
+        DATA_INVARIANT(
+          bv.size() == op.size(),
+          std::string("size of value operand does not match:\n") +
+            "result size: " + std::to_string(bv.size()) +
+            "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
 
         literalt value_literal=bv_utils.equal(bv, op);
 
diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp
index 95a379a5a95..11dda842f17 100644
--- a/src/solvers/flattening/boolbv_equality.cpp
+++ b/src/solvers/flattening/boolbv_equality.cpp
@@ -8,10 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-#include <iostream>
-
 #include <util/std_expr.h>
 #include <util/base_type.h>
+#include <util/invariant.h>
 
 #include <langapi/language_util.h>
 
@@ -19,12 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
-  if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns))
-  {
-    std::cout << "######### lhs: " << expr.lhs().pretty() << '\n';
-    std::cout << "######### rhs: " << expr.rhs().pretty() << '\n';
-    throw "equality without matching types";
-  }
+  const bool is_base_type_eq =
+    base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
+  DATA_INVARIANT(
+    is_base_type_eq,
+    std::string("equality without matching types:\n") + "######### lhs: " +
+      expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty());
 
   // see if it is an unbounded array
   if(is_unbounded_array(expr.lhs().type()))
@@ -43,14 +42,12 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
   const bvt &bv0=convert_bv(expr.lhs());
   const bvt &bv1=convert_bv(expr.rhs());
 
-  if(bv0.size()!=bv1.size())
-  {
-    std::cerr << "lhs: " << expr.lhs().pretty() << '\n';
-    std::cerr << "lhs size: " << bv0.size() << '\n';
-    std::cerr << "rhs: " << expr.rhs().pretty() << '\n';
-    std::cerr << "rhs size: " << bv1.size() << '\n';
-    throw "unexpected size mismatch on equality";
-  }
+  DATA_INVARIANT(
+    bv0.size() == bv1.size(),
+    std::string("unexpected size mismatch on equality:\n") + "lhs: " +
+      expr.lhs().pretty() + '\n' + "lhs size: " + std::to_string(bv0.size()) +
+      '\n' + "rhs: " + expr.rhs().pretty() + '\n' +
+      "rhs size: " + std::to_string(bv1.size()));
 
   if(bv0.empty())
   {
@@ -68,24 +65,23 @@ literalt boolbvt::convert_verilog_case_equality(
   // This is 4-valued comparison, i.e., z===z, x===x etc.
   // The result is always Boolean.
 
-  if(!base_type_eq(expr.lhs().type(), expr.rhs().type(), ns))
-  {
-    std::cout << "######### lhs: " << expr.lhs().pretty() << '\n';
-    std::cout << "######### rhs: " << expr.rhs().pretty() << '\n';
-    throw "verilog_case_equality without matching types";
-  }
+  const bool is_base_type_eq =
+    base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
+  DATA_INVARIANT(
+    is_base_type_eq,
+    std::string("verilog_case_equality without matching types:\n") +
+      "######### lhs: " + expr.lhs().pretty() + '\n' +
+      "######### rhs: " + expr.rhs().pretty());
 
   const bvt &bv0=convert_bv(expr.lhs());
   const bvt &bv1=convert_bv(expr.rhs());
 
-  if(bv0.size()!=bv1.size())
-  {
-    std::cerr << "lhs: " << expr.lhs().pretty() << '\n';
-    std::cerr << "lhs size: " << bv0.size() << '\n';
-    std::cerr << "rhs: " << expr.rhs().pretty() << '\n';
-    std::cerr << "rhs size: " << bv1.size() << '\n';
-    throw "unexpected size mismatch on verilog_case_equality";
-  }
+  DATA_INVARIANT(
+    bv0.size() == bv1.size(),
+    std::string("unexpected size mismatch on verilog_case_equality:\n") +
+      "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " +
+      std::to_string(bv0.size()) + '\n' + "rhs: " + expr.rhs().pretty() + '\n' +
+      "rhs size: " + std::to_string(bv1.size()));
 
   if(expr.id()==ID_verilog_case_inequality)
     return !bv_utils.equal(bv0, bv1);
diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp
index d6609691df2..6f5b762c17d 100644
--- a/src/solvers/flattening/boolbv_floatbv_op.cpp
+++ b/src/solvers/flattening/boolbv_floatbv_op.cpp
@@ -88,12 +88,9 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
   bvt bv2=convert_bv(op2);
 
   const typet &type=ns.follow(expr.type());
-
-  if(op0.type()!=type || op1.type()!=type)
-  {
-    std::cerr << expr.pretty() << '\n';
-    throw "float op with mixed types";
-  }
+  DATA_INVARIANT(
+    op0.type() == type && op1.type() == type,
+    "float op with mixed types:\n" + expr.pretty());
 
   float_utilst float_utils(prop);
 
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 2d8d0254599..86641b8ffa4 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -226,8 +226,6 @@ void bv_refinementt::check_SAT(approximationt &a)
               << "==" << integer2binary(result.pack(), spec.width()) << eom;
     #endif
 
-    // if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); }
-
     if(a.over_state<config_.max_node_refinement)
     {
       bvt r;
diff --git a/src/solvers/sat/cnf.cpp b/src/solvers/sat/cnf.cpp
index bed97954bac..7250131a384 100644
--- a/src/solvers/sat/cnf.cpp
+++ b/src/solvers/sat/cnf.cpp
@@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "cnf.h"
 
 #include <algorithm>
-#include <cassert>
-#include <iostream>
 #include <set>
 
+#include <util/invariant.h>
+
 // #define VERBOSE
 
 /// Tseitin encoding of conjunction of two literals
@@ -426,10 +426,12 @@ bool cnft::process_clause(const bvt &bv, bvt &dest)
   for(const auto l : bv)
   {
     // we never use index 0
-    assert(l.var_no()!=0);
+    INVARIANT(l.var_no() != 0, "variable 0 must not be used");
 
     // we never use 'unused_var_no'
-    assert(l.var_no()!=literalt::unused_var_no());
+    INVARIANT(
+      l.var_no() != literalt::unused_var_no(),
+      "variable 'unused_var_no' must not be used");
 
     if(l.is_true())
       return true; // clause satisfied
@@ -437,11 +439,10 @@ bool cnft::process_clause(const bvt &bv, bvt &dest)
     if(l.is_false())
       continue; // will remove later
 
-    if(l.var_no()>=_no_variables)
-      std::cout << "l.var_no()=" << l.var_no()
-                << " _no_variables=" << _no_variables << '\n';
-
-    assert(l.var_no()<_no_variables);
+    INVARIANT(
+      l.var_no() < _no_variables,
+      "unknown variable " + std::to_string(l.var_no()) +
+        " (no_variables = " + std::to_string(_no_variables) + " )");
   }
 
   // now copy
diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
index b439577c270..84d3893eaeb 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.cpp
+++ b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -11,17 +11,21 @@ Author: Alex Groce
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
+
+#ifdef DEBUG
 #include <iostream>
+#endif
 
 void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out)
 {
-  double d_sum=0;
+  double d_sum = 0;
 
-  // std::cout << "enter: No Lit.=" << no_variables () << "\n";
+#ifdef DEBUG
+  std::cout << "enter: No Lit.=" << no_variables() << "\n";
+#endif
 
-  for(std::map<literalt, unsigned>::const_iterator it=pb_constraintmap.begin();
-      it!=pb_constraintmap.end(); ++it)
-    d_sum += ((*it).second);
+  for(const auto &lit_entry : pb_constraintmap)
+    d_sum += lit_entry.second;
 
   if(!optimize)
   {
@@ -45,44 +49,50 @@ void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out)
 
   for(const auto &lit_entry : pb_constraintmap)
   {
-    int dimacs_lit=lit_entry.first.dimacs();
+    const int dimacs_lit = lit_entry.first.dimacs();
     out << "v" << dimacs_lit << " c" << lit_entry.second << "\n";
   }
 
-  // std::cout << "exit: No Lit.=" << no_variables () << "\n";
+#ifdef DEBUG
+  std::cout << "exit: No Lit.=" << no_variables() << "\n";
+#endif
 }
 
 bool pbs_dimacs_cnft::pbs_solve()
 {
-  // std::cout << "solve: No Lit.=" << no_variables () << "\n";
+#ifdef DEBUG
+  std::cout << "solve: No Lit.=" << no_variables() << "\n";
+#endif
 
   std::string command;
 
   if(!pbs_path.empty())
   {
     command += pbs_path;
-    if(command.substr(command.length(), 1)!="/")
+    if(command.substr(command.length(), 1) != "/")
       command += "/";
   }
 
   command += "pbs";
 
-  // std::cout << "PBS COMMAND IS: " << command << "\n";
-  /*
-    if (!(getenv("PBS_PATH")==NULL))
-    {
+#ifdef DEBUG
+  std::cout << "PBS COMMAND IS: " << command << "\n";
+#endif
+#if 0
+  if (!(getenv("PBS_PATH")==NULL))
+  {
     command=getenv("PBS_PATH");
-    }
-    else
-    {
+  }
+  else
+  {
     error ("Unable to read PBS_PATH environment variable.\n");
     return false;
-    }
-  */
+  }
+#endif
 
   command += " -f temp.cnf";
 
-  #if 1
+#if 1
   if(optimize)
   {
     if(binary_search)
@@ -91,7 +101,10 @@ bool pbs_dimacs_cnft::pbs_solve()
     }
     else
     {
-      // std::cout << "NO BINARY SEARCH" << "\n";
+#ifdef DEBUG
+      std::cout << "NO BINARY SEARCH"
+                << "\n";
+#endif
       command += " -S 1000 -D 1 -I -a";
     }
   }
@@ -99,19 +112,19 @@ bool pbs_dimacs_cnft::pbs_solve()
   {
     command += " -S 1000 -D 1 -a";
   }
-  #else
+#else
   command += " -z";
-  #endif
+#endif
 
   command += " -a > temp.out";
 
-  int res=system(command.c_str());
-  CHECK_RETURN(0==res);
+  const int res = system(command.c_str());
+  CHECK_RETURN(0 == res);
 
   std::ifstream file("temp.out");
   std::string line;
   int v;
-  bool satisfied=false;
+  bool satisfied = false;
 
   if(file.fail())
   {
@@ -119,60 +132,74 @@ bool pbs_dimacs_cnft::pbs_solve()
     return false;
   }
 
-  opt_sum=-1;
+  opt_sum = -1;
 
-  while(file && !file.eof ())
+  while(file && !file.eof())
+  {
+    std::getline(file, line);
+    if(
+      strstr(line.c_str(), "Variable Assignments Satisfying CNF Formula:") !=
+      nullptr)
     {
-      std::getline(file, line);
-      if(strstr(line.c_str(),
-                "Variable Assignments Satisfying CNF Formula:")!=nullptr)
-        {
-          // print ("Reading assignments...\n");
-          // std::cout << "No literals: " << no_variables() << "\n";
-          satisfied=true;
-          assigned.clear();
-          for(size_t i=0; (file && (i < no_variables())); ++i)
-            {
-              file >> v;
-              if(v > 0)
-                {
-                  // std::cout << v << " ";
-                  assigned.insert(v);
-                }
-            }
-          // std::cout << "\n";
-          // print ("Finished reading assignments.\n");
-        }
-      else if(strstr(line.c_str(), "SAT... SUM")!=nullptr)
-        {
-          // print (line);
-          sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
-        }
-      else if(strstr(line.c_str(), "SAT - All implied")!=nullptr)
-        {
-          // print (line);
-          sscanf(
-            line.c_str(),
-            "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d",
-            &opt_sum);
-        }
-      else if(strstr(line.c_str(), "SAT... Solution")!=nullptr)
-        {
-          // print(line);
-          sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
-        }
-      else if(strstr(line.c_str(), "Optimal Soln")!=nullptr)
+#ifdef DEBUG
+      std::cout << "Reading assignments...\n";
+      std::cout << "No literals: " << no_variables() << "\n";
+#endif
+      satisfied = true;
+      assigned.clear();
+      for(size_t i = 0; (file && (i < no_variables())); ++i)
+      {
+        file >> v;
+        if(v > 0)
         {
-          // print(line);
-          if(strstr(line.c_str(), "time out")!=nullptr)
-            {
-              status() << "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT."
-                       << eom;
-              return satisfied;
-            }
-          sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
+#ifdef DEBUG
+          std::cout << v << " ";
+#endif
+          assigned.insert(v);
         }
+      }
+#ifdef DEBUG
+      std::cout << "\n";
+      std::cout << "Finished reading assignments.\n";
+#endif
+    }
+    else if(strstr(line.c_str(), "SAT... SUM") != nullptr)
+    {
+#ifdef DEBUG
+      std::cout << line;
+#endif
+      sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
+    }
+    else if(strstr(line.c_str(), "SAT - All implied") != nullptr)
+    {
+#ifdef DEBUG
+      std::cout << line;
+#endif
+      sscanf(
+        line.c_str(),
+        "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d",
+        &opt_sum);
+    }
+    else if(strstr(line.c_str(), "SAT... Solution") != nullptr)
+    {
+#ifdef DEBUG
+      std::cout << line;
+#endif
+      sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
     }
+    else if(strstr(line.c_str(), "Optimal Soln") != nullptr)
+    {
+#ifdef DEBUG
+      std::cout << line;
+#endif
+      if(strstr(line.c_str(), "time out") != nullptr)
+      {
+        status() << "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT." << eom;
+        return satisfied;
+      }
+      sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
+    }
+  }
 
   return satisfied;
 }
@@ -191,21 +218,18 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
   pbfile.close();
 
   // We start counting at 1, thus there is one variable fewer.
-  messaget::status() <<
-    (no_variables()-1) << " variables, " <<
-    clauses.size() << " clauses" << eom;
+  messaget::status() << (no_variables() - 1) << " variables, " << clauses.size()
+                     << " clauses" << eom;
 
-  bool result=pbs_solve();
+  const bool result = pbs_solve();
 
   if(!result)
   {
-    messaget::status() <<
-      "PBS checker: system is UNSATISFIABLE" << eom;
+    messaget::status() << "PBS checker: system is UNSATISFIABLE" << eom;
   }
   else
   {
-    messaget::status() <<
-      "PBS checker: system is SATISFIABLE";
+    messaget::status() << "PBS checker: system is SATISFIABLE";
     if(optimize)
       messaget::status() << " (distance " << opt_sum << ")";
     messaget::status() << eom;
@@ -219,40 +243,50 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
 
 tvt pbs_dimacs_cnft::l_get(literalt a) const
 {
-  int dimacs_lit=a.dimacs();
+  int dimacs_lit = a.dimacs();
 
-  // std::cout << a << " / " << dimacs_lit << "=";
+#ifdef DEBUG
+  std::cout << a << " / " << dimacs_lit << "=";
+#endif
 
-  bool neg=(dimacs_lit < 0);
+  const bool neg = (dimacs_lit < 0);
   if(neg)
-    dimacs_lit=-dimacs_lit;
+    dimacs_lit = -dimacs_lit;
 
-  std::set<int>::const_iterator f=assigned.find(dimacs_lit);
+  std::set<int>::const_iterator f = assigned.find(dimacs_lit);
 
   if(!neg)
+  {
+    if(f == assigned.end())
     {
-      if(f==assigned.end())
-        {
-          // std::cout << "FALSE" << "\n";
-          return tvt(false);
-        }
-      else
-        {
-          // std::cout << "TRUE" << "\n";
-          return tvt(true);
-        }
+#ifdef DEBUG
+      std::cout << "FALSE\n";
+#endif
+      return tvt(false);
+    }
+    else
+    {
+#ifdef DEBUG
+      std::cout << "TRUE\n";
+#endif
+      return tvt(true);
     }
+  }
   else
+  {
+    if(f != assigned.end())
     {
-      if(f!=assigned.end())
-        {
-          // std::cout << "FALSE" << "\n";
-          return tvt(false);
-        }
-      else
-        {
-          // std::cout << "TRUE" << "\n";
-          return tvt(true);
-        }
+#ifdef DEBUG
+      std::cout << "FALSE\n";
+#endif
+      return tvt(false);
+    }
+    else
+    {
+#ifdef DEBUG
+      std::cout << "TRUE\n";
+#endif
+      return tvt(true);
     }
+  }
 }
diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp
index ef61ff89a78..9477d8d4a6c 100644
--- a/src/util/cmdline.cpp
+++ b/src/util/cmdline.cpp
@@ -8,9 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cmdline.h"
 
-#include <cassert>
-#include <cstdlib>
-#include <iostream>
+#include <util/invariant.h>
 
 cmdlinet::cmdlinet()
 {
@@ -124,11 +122,8 @@ bool cmdlinet::parse(int argc, const char **argv, const char *optstring)
   {
     optiont option;
 
-    if(optstring[0]==':')
-    {
-      std::cerr << "cmdlinet::parse: Invalid option string\n";
-      abort();
-    }
+    DATA_INVARIANT(
+      optstring[0] != ':', "cmdlinet::parse: Invalid option string\n");
 
     if(optstring[0]=='(')
     {