19 Commits

Author	SHA1	Message	Date
Pawel Gebal	d4be1d9c2f	Add --print-smt flag to output SMTChecker SMTLIB code	2023-06-16 14:04:07 +02:00
Pawel Gebal	f15b826431	Add optional bounds to unroll loops in BMC model checker	2023-06-02 18:32:38 +02:00
Leo Alt	aacbe72079	group unsupported warnings	2023-03-15 17:06:06 +01:00
Leo Alt	21c0f78650	Report safe properties in BMC and CHC	2023-03-09 14:59:32 +01:00
Leo Alt	8d91ccf028	[SMTChecker] Add a new trusted mode which assumes that code that is ... available at compile time is trusted.	2023-02-06 17:02:33 +01:00
Leo Alt	24df40de9a	Allow running Eldarica from the command line	2022-11-22 21:16:45 +01:00
Leo Alt	37215ffcfd	Add SMTCheckerTest isoltest option to ignore invariants	2021-10-26 11:30:30 +02:00
Leo Alt	d419c30ca6	Add errorCode list to invariants report	2021-10-26 11:30:30 +02:00
Leo Alt	bc90533c93	Add invariants to ModelCheckerSettings	2021-10-26 11:30:30 +02:00
Leo Alt	ee6285d6d7	Do not create VCs for underoverflow by default for Sol >=0.8	2021-08-09 14:12:31 +02:00
Leo Alt	08c065ee04	Add option divModWithSlacks	2021-08-06 15:50:25 +02:00
Leo Alt	685d7a8c99	Bundle all unproved targets in a single message and only show all if setting chooses that	2021-08-04 13:54:50 +02:00
Leo Alt	6c8ecfa82c	Add option to choose solver	2021-07-27 17:14:21 +02:00
Kamil Śliwak	7d16c7b127	Equality operators for ModelCheckerSettings and ImportRemapper	2021-07-06 17:17:18 +02:00
Leonardo Alt	dd1865873e	Choose contracts to be analyzed by the SMTChecker	2021-04-21 10:34:14 +02:00
Leonardo Alt	e3abde43f5	Change settings.modelChecker.targets to take an array instead of string	2021-04-19 17:53:03 +02:00
Leonardo Alt	b753cb6120	Deprecate pragma experimental SMTChecker	2021-04-08 21:03:38 +02:00
Leonardo Alt	dbd067d6db	Report out of bounds index access	2021-03-30 10:28:48 +02:00
Leonardo Alt	3b23cadbdc	Add CLI and JSON option to select SMTChecker targets	2021-01-20 17:35:37 +01:00