From b6c80e8b00035b0810bcd08f121ad09c63043c95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jul 2022 04:28:28 +0200 Subject: [PATCH] fix #6193 --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5f630d814..2731d6d27 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3414,7 +3414,7 @@ namespace z3 { } }; - constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) { + inline constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) { array cons(cs.size()); for (unsigned i = 0; i < cs.size(); ++i) cons[i] = cs[i];