diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 6296d344a..cb016e263 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -546,7 +546,7 @@ expr * array_decl_plugin::get_some_value(sort * s) { return m_manager->mk_app(m_family_id, OP_CONST_ARRAY, 1, &p, 1, &v); } -bool array_decl_plugin::is_fully_interp(sort const * s) const { +bool array_decl_plugin::is_fully_interp(sort * s) const { SASSERT(s->is_sort_of(m_family_id, ARRAY_SORT)); unsigned sz = get_array_arity(s); for (unsigned i = 0; i < sz; i++) { diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 0febb82a4..0704fe56a 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -127,7 +127,7 @@ class array_decl_plugin : public decl_plugin { virtual expr * get_some_value(sort * s); - virtual bool is_fully_interp(sort const * s) const; + virtual bool is_fully_interp(sort * s) const; }; class array_recognizers {