cerc-io/solidity
11
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
23,867 Commits 348 Branches 121 Tags
smtlib-interface-for-everything
Commit Graph
44 Commits
Author SHA1 Message Date
Martin Blicha a4b4e70b67 Get invariants from eldarica 2023-09-05 12:39:20 +02:00
Martin Blicha 497ca183b4 Small cleanup 2023-09-05 12:39:19 +02:00
Martin Blicha 8e0e2cb1ae Throw when trying to read past the end of SMTLib stream 2023-09-05 12:39:19 +02:00
Martin Blicha 4101c67cba Update to let inlining 2023-09-05 12:39:19 +02:00
Martin Blicha af1acaba64 Refactor SMTLib parser to separate file 2023-09-05 12:39:19 +02:00
Martin Blicha 8c99c125c4 Add support for parsing invariants 2023-09-05 12:39:19 +02:00
Martin Blicha 3f22118bbe More checks 2023-09-05 12:39:19 +02:00
Martin Blicha 01ed412714 Stronger checks 2023-09-05 12:39:19 +02:00
Martin Blicha 0c13b7ee8f Turn asserts into solAsserts 2023-09-05 12:39:19 +02:00
Martin Blicha 5569aaee78 Fix coding style 2023-09-05 12:39:19 +02:00
Martin Blicha 4ecaa476fd Handle custom tuple sorts in a general way 2023-09-05 12:39:19 +02:00
Martin Blicha 742642ebae Use answer from second Z3 call only when solved 2023-09-05 12:39:19 +02:00
Martin Blicha 0fbeb3a69d Throw exception on unhandled cases in SMT-LIB Expression conversion 2023-09-05 12:39:19 +02:00
Martin Blicha 779db2d84f Use shared pointers, not raw pointers, for caching sorts 2023-09-05 12:39:19 +02:00
Martin Blicha b65c37029d Fix parsing array expressions from SMT-LIB proof 2023-09-05 12:39:19 +02:00
Martin Blicha d773e76704 Remove outdated FIXME 2023-09-05 12:39:19 +02:00
Martin Blicha 451b6f8ced Fix handling of structs in SMT-LIB CEX 2023-09-05 12:39:19 +02:00
Martin Blicha 9339b7074a Fix parsing of let expression to allow shadowing values 2023-09-05 12:39:19 +02:00
Martin Blicha 92689e4256 Fix code style problems 2023-09-05 12:39:19 +02:00
Martin Blicha 8ea8a1eb99 Cache sorts already in SMTLib2Interface 
This allows us to ask for a sort of a sort from its string
representation parsed from an SMT-LIB solver response
 2023-09-05 12:39:19 +02:00
Martin Blicha 6acbe2ec35 Towards translating proof from SMT-LIB response 2023-09-05 12:39:19 +02:00
Martin Blicha 479bb9c3de Fix missing std 2023-09-05 12:39:19 +02:00
Martin Blicha 2195b5e57a Solve UNSAT queries again with proof production enabled 2023-09-05 12:39:19 +02:00
Martin Blicha 1d60559551 Use same spacer parameters as before 2023-09-05 12:39:19 +02:00
Martin Blicha d9dc8f475e Enable resource limit for Z3 2023-09-05 12:39:19 +02:00
Martin Blicha f4b849972c Remove smtlib2 solver option 2023-09-05 12:39:17 +02:00
Martin Blicha cabec89872 Removing SMT portfolio 2023-09-05 12:37:56 +02:00
Martin Blicha 1e190abf6e Initial work on unified way to interact with solvers 2023-09-05 12:37:56 +02:00
Nikola Matic 62723b7534 Purge using namespace std in libsmtutil and libsolc 2023-07-12 14:09:19 +02:00
Pawel Gebal d4be1d9c2f Add --print-smt flag to output SMTChecker SMTLIB code 2023-06-16 14:04:07 +02:00
Leo Alt 24df40de9a Allow running Eldarica from the command line 2022-11-22 21:16:45 +01:00
Marenz f7cc29bec1 Add std:: qualifier to move() calls 2022-08-30 11:12:15 +02:00
Leo Alt 9a87680d21 Add invariant to the solver results 2021-10-26 11:30:30 +02:00
Kamil Śliwak 7f7107405f Try out the new assertion macro variants with less arguments 2021-10-04 12:05:00 +02:00
Leo Alt f7b045b886 review 2021-05-26 22:12:49 +02:00
Leo Alt daea5f886d Fix CHCSmtLib2Interface 2021-05-26 22:12:49 +02:00
Daniel Kirchner cb72d76aaf Add const ref to prevent segfaults. 2020-12-04 14:57:46 +01:00
Leonardo Alt d03ddeb0fa [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
Leonardo Alt 23ee011c56 [SMTChecker] Fix imports 2020-09-11 13:34:46 +02:00
Leonardo Alt 744905525f Convert z3 cex graph into STL 2020-07-23 18:49:03 +02:00
Sachin Grover b7adb2aa42 Add SPDX license identifier if not present already in source file 
Fixes: #9220
 2020-07-17 20:24:12 +05:30
Leonardo Alt 25de3975ce Add SMTLogicException 2020-05-20 12:55:19 +02:00
Leonardo Alt 45eba27424 Rename namespace 2020-05-20 12:55:18 +02:00
Leonardo Alt 087605ea02 Create libsmtutil 2020-05-20 12:55:18 +02:00