mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
This commit is contained in:
parent
18e4546404
commit
9c5ef79701
|
@ -72,7 +72,7 @@ namespace euf {
|
|||
void * etable::mk_table_for(unsigned arity, func_decl * d) {
|
||||
void * r;
|
||||
SASSERT(d->get_arity() >= 1);
|
||||
SASSERT(arity >= d->get_arity() || d->is_associative());
|
||||
SASSERT(arity >= d->get_arity() || d->is_associative() || d->is_left_associative());
|
||||
switch (arity) {
|
||||
case 1:
|
||||
r = TAG(void*, alloc(unary_table), UNARY);
|
||||
|
|
Loading…
Reference in a new issue