From 808dade2b6be43516ddb7bad52c6ffbb4aba9588 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Apr 2018 19:07:11 +0000 Subject: [PATCH] Provide suitable diagnostics for equality-without-matching-types --- src/solvers/flattening/boolbv_equality.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 8621efa3cbe..2e7ac9aa500 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -12,16 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "bv_conversion_exceptions.h" #include "flatten_byte_operators.h" literalt boolbvt::convert_equality(const equal_exprt &expr) { 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()); + if(!is_base_type_eq) + { + const std::string error_msg = + std::string("equality without matching types:\n") + "######### lhs: " + + expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty(); + throw bitvector_conversion_exceptiont(error_msg, expr); + } // see if it is an unbounded array if(is_unbounded_array(expr.lhs().type()))