cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fix parsing array expressions from SMT-LIB proof

Browse Source
This commit is contained in:
Martin Blicha 2023-07-27 10:26:02 +02:00
parent d773e76704
commit b65c37029d
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -351,6 +351,10 @@ namespace
auto sort = toSort(_subExpr.front()); auto sort = toSort(_subExpr.front());
auto sortSort = std::make_shared<SortSort>(sort); auto sortSort = std::make_shared<SortSort>(sort);
return Expression::tuple_constructor(Expression(sortSort), arguments); 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<SortSort>(sort);
return Expression::tuple_constructor(Expression(sortSort), arguments);
} else { } else {
std::set<std::string> boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", std::set<std::string> boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=",
"=>"}; "=>"};