smt: fix crash in isConcat() with nargs > 2
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -364,9 +364,13 @@ bool expr::isIf(expr &cond, expr &then, expr &els) const {
bool expr::isConcat(expr &a, expr &b) const {
if (auto app = isAppOf(Z3_OP_CONCAT)) {
- assert(Z3_get_domain_size(ctx(), decl()) == 2);
+ auto nargs = Z3_get_domain_size(ctx(), decl());
+ assert(nargs >= 2);
a = Z3_get_app_arg(ctx(), app, 0);
b = Z3_get_app_arg(ctx(), app, 1);
+ for (unsigned i = 2; i < nargs; ++i) {
+ b = b.concat(Z3_get_app_arg(ctx(), app, i));
+ }
return true;
}
return false;

smt: fix crash in isConcat() with nargs > 2