diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index ac1baba3c..c98e4414d 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -351,6 +351,10 @@ namespace auto sort = toSort(_subExpr.front()); auto sortSort = std::make_shared(sort); return Expression::tuple_constructor(Expression(sortSort), arguments); + } else if (op.find("array_tuple") != std::string::npos) { + auto sort = toSort(_subExpr.front()); + auto sortSort = std::make_shared(sort); + return Expression::tuple_constructor(Expression(sortSort), arguments); } else { std::set boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", "=>"};