Replace std::cout for errors with messaget::error()

Also replace assert(false) with throw while I'm there.

Author: smowton

src/solvers/flattening/arrays.cpp

@@ -84,7 +84,7 @@ literalt arrayst::record_array_equality(
   // check types
   if(!base_type_eq(op0.type(), op1.type(), ns))
   {
-    std::cout << equality.pretty() << std::endl;
+    prop.error() << equality.pretty() << messaget::eom;
     throw "record_array_equality got equality without matching types";
   }
 
@@ -174,7 +174,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, a.op0().type(), ns))
     {
-      std::cout << a.pretty() << std::endl;
+      prop.error() << a.pretty() << messaget::eom;
       throw "collect_arrays got 'with' without matching types";
     }
 
@@ -196,7 +196,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, a.op0().type(), ns))
     {
-      std::cout << a.pretty() << std::endl;
+      prop.error() << a.pretty() << messaget::eom;
       throw "collect_arrays got 'update' without matching types";
     }
 
@@ -220,14 +220,14 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, a.op1().type(), ns))
     {
-      std::cout << a.pretty() << std::endl;
+      prop.error() << a.pretty() << messaget::eom;
       throw "collect_arrays got if without matching types";
     }
 
     // check types
     if(!base_type_eq(array_type, a.op2().type(), ns))
     {
-      std::cout << a.pretty() << std::endl;
+      prop.error() << a.pretty() << messaget::eom;
       throw "collect_arrays got if without matching types";
     }
 
@@ -678,8 +678,8 @@ void arrayst::add_array_constraints_with(
 
     if(index_expr.type()!=value.type())
     {
-      std::cout << expr.pretty() << std::endl;
-      assert(false);
+      prop.error() << expr.pretty() << messaget::eom;
+      throw "index_expr and value types should match";
     }
 
     lazy_constraintt lazy(
@@ -774,8 +774,8 @@ void arrayst::add_array_constraints_update(
 
     if(index_expr.type()!=value.type())
     {
-      std::cout << expr.pretty() << std::endl;
-      assert(false);
+      prop.error() << expr.pretty() << messaget::eom;
+      throw "index_expr and value types should match";
     }
 
     set_to_true(equal_exprt(index_expr, value));