diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 0ac0a11204a..b5904e7a664 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -257,10 +257,11 @@ void ansi_c_convert_typet::read_rec(const typet &type) { if( operand.id() != ID_symbol && operand.id() != ID_ptrmember && - operand.id() != ID_dereference) + operand.id() != ID_member && operand.id() != ID_dereference) { error().source_location = source_location; - error() << "illegal target in assigns clause" << eom; + error() << "illegal target (" << operand.id_string() + << ") in assigns clause" << eom; throw 0; } } diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 3bda86f2cfa..fc3b1484b96 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -47,7 +47,7 @@ class boolbvt:public arrayst message_handlert &message_handler, bool get_array_constraints = false) : arrayst(_ns, _prop, message_handler, get_array_constraints), - unbounded_array(unbounded_arrayt::U_AUTO), + unbounded_array(unbounded_arrayt::U_NONE), bv_width(_ns), bv_utils(_prop), functions(*this),