#5532

Z3Prover · Sep 4, 2021 · 9c5ef79 · 9c5ef79
1 parent 18e4546
commit 9c5ef79
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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);