mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ee4ae33ac4
commit
10f734357e
|
@ -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++) {
|
||||
|
|
|
@ -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 {
|
||||
|
|
Loading…
Reference in a new issue