From c9ca31168df0931781bb44f18572c21a87f34fd6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 8 Dec 2022 00:07:01 +0000 Subject: [PATCH] Enable automatic limit for array-as-uninterpreted-function Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way. This reverts #6232, but now includes additional changes to the array theory to handle nested struct members no different from members of a top-level struct. Fixes: #2018 --- src/solvers/flattening/arrays.cpp | 11 +---------- src/solvers/flattening/boolbv.h | 2 +- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 023f1805fe1..cb035f2a530 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -195,12 +195,6 @@ void arrayst::collect_arrays(const exprt &a) } else if(a.id()==ID_member) { - const auto &struct_op = to_member_expr(a).struct_op(); - - DATA_INVARIANT( - struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol, - "unexpected array expression: member with '" + struct_op.id_string() + - "'"); } else if(a.id()==ID_constant || a.id()==ID_array || @@ -494,10 +488,7 @@ void arrayst::add_array_constraints( expr.id()==ID_string_constant) { } - else if( - expr.id() == ID_member && - (to_member_expr(expr).struct_op().id() == ID_symbol || - to_member_expr(expr).struct_op().id() == ID_nondet_symbol)) + else if(expr.id() == ID_member) { } else if(expr.id()==ID_byte_update_little_endian || diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 1636dd67ffa..6eaf6c48643 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -49,7 +49,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_NONE), + unbounded_array(unbounded_arrayt::U_AUTO), bv_width(_ns), bv_utils(_prop), functions(*this),