18 Commits

Author	SHA1	Message	Date
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	88030c6568	[SMTChecker] Refactor verification targets	2020-07-10 10:28:49 +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
a3d4	7cae074b8a	Add error IDs to BMC	2020-05-12 11:39:18 +02:00
Leonardo Alt	6451a4d2a0	Move VerificationTarget and add BMCVerificationTarget	2020-02-12 11:47:58 -03:00
Christian Parpart	6b23412fae	C++ namespace cleanup (except tests).	2020-01-07 15:51:50 +01:00
Leonardo Alt	f4f83690f3	Replace some shared_ptr by unique_ptr or raw pointers	2020-01-06 14:16:49 +01:00
chriseth	e061f1e743	Merge remote-tracking branch 'origin/develop' into HEAD	2019-12-05 16:44:26 +01:00
Leonardo Alt	48c3a5c225	[SMTChecker] Create options to choose SMT solver in runtime	2019-12-04 17:31:44 +01:00
Leonardo Alt	ddc478e3e4	Add CallbackKind and use it for the SMT solver	2019-11-21 22:10:21 +00:00
Leonardo Alt	4214cd1354	[SMTChecker] Fix ICE when reporting cex concerning state vars from different source files	2019-08-10 20:56:52 +02:00
Leonardo Alt	7b22496b1f	[SMTChecker] Fix ICE when inlining functions that use state vars and are in a different source	2019-08-09 17:50:52 +02:00
Leonardo	264035f0dd	Merge pull request #7120 from ethereum/smt_refactor_inlining ... [SMTChecker] Refactor function inlining	2019-07-22 14:20:32 +02:00
Leonardo Alt	03cc124f32	Add CHC skeleton	2019-07-19 11:52:05 +02:00
Leonardo Alt	382df64899	[SMTChecker] Refactor function inlining	2019-07-18 13:56:48 +02:00
Leonardo Alt	b0818bd002	[SMTChecker] Move solver pointer from SMTEncoder to BMC	2019-07-02 12:06:52 +02:00
Leonardo Alt	3cb4ed83c1	[SMTChecker] Split SMTChecker into SMTEncoder and BMC	2019-07-01 15:05:03 +02:00