From 9c5ef79701d26fa6c9413a5be4493982916d0638 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Sep 2021 09:05:49 -0700 Subject: [PATCH] #5532 --- src/ast/euf/euf_etable.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index 43ad52726..cfc99e4a0 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -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);