removed dependency on linking module

Author: Daniel Kroening

src/solvers/smt1/smt1_conv.cpp

@@ -21,8 +21,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 
-#include <linking/zero_initializer.h>
-
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
 #include <solvers/flattening/flatten_byte_operators.h>
@@ -1555,7 +1553,7 @@ void smt1_convt::convert_typecast(
       convert_expr(src, true);
       out << " ";
       convert_expr(
-        zero_initializer(src_type, expr.source_location(), ns),
+        from_integer(0, src_type),
         true);
       out << "))";
     }
@@ -1584,7 +1582,7 @@ void smt1_convt::convert_typecast(
       convert_expr(src, true);
       out << " ";
       convert_expr(
-        zero_initializer(src_type, expr.source_location(), ns),
+        from_integer(0, src_type),
         true);
       out << ")) "; // not, =
       out << " bv1[" << to_width << "]";

src/solvers/smt2/smt2_conv.cpp

@@ -22,8 +22,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 
-#include <linking/zero_initializer.h>
-
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
@@ -2089,8 +2087,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       out << "(not (= ";
       convert_expr(src);
       out << " ";
-      convert_expr(
-        zero_initializer(src_type, expr.source_location(), ns));
+      convert_expr(from_integer(0, src_type));
       out << "))";
     }
     else if(src_type.id()==ID_floatbv)
@@ -2116,8 +2113,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
     out << "(not (= ";
     convert_expr(src);
     out << " ";
-    convert_expr(
-      zero_initializer(src_type, expr.source_location(), ns));
+    convert_expr(from_integer(0, src_type));
     out << ")) "; // not, =
     out << " (_ bv1 " << to_width << ")";
     out << " (_ bv0 " << to_width << ")";

src/util/simplify_expr.cpp

@@ -32,8 +32,6 @@ Author: Daniel Kroening, [email protected]
 #include "endianness_map.h"
 #include "simplify_utils.h"
 
-#include <linking/zero_initializer.h>
-
 // #define DEBUGX
 
 #ifdef DEBUGX
@@ -277,8 +275,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
     inequality.add_source_location()=expr.source_location();
     inequality.lhs()=expr.op0();
-    inequality.rhs()=
-      zero_initializer(expr.op0().type(), expr.source_location(), ns);
+    inequality.rhs()=from_integer(0, op_type);
     assert(inequality.rhs().is_not_nil());
     simplify_node(inequality);
     expr.swap(inequality);
@@ -294,8 +291,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
     inequality.add_source_location()=expr.source_location();
     inequality.lhs()=expr.op0();
-    inequality.rhs()=
-      zero_initializer(expr.op0().type(), expr.source_location(), ns);
+    inequality.rhs()=from_integer(0, op_type);
     assert(inequality.rhs().is_not_nil());
     simplify_node(inequality);
     expr.op0()=inequality;