From 3dc822c12706e2cfe3dd392747098b6c93295881 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 1 Feb 2020 18:48:27 -0800
Subject: [PATCH] fix #2903

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index bd0679c85..10e7bc367 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -819,7 +819,8 @@ namespace datatype {
             for (constructor const* c : d) {
                 ptr_vector<param_size::size> s_mul;
                 for (accessor const* a : *c) {
-                    s_mul.push_back(get_sort_size(d.params(), a->range()));
+                    auto* sz = get_sort_size(d.params(), a->range());
+                    if (sz) s_mul.push_back(sz);
                 }
                 s_add.push_back(param_size::size::mk_times(s_mul));
             }