59 Commits

Author	SHA1	Message	Date
Denis Merigoux	3f49824150	Merge branch 'master' into c_backend	2022-04-04 18:02:33 +02:00
Denis Merigoux	31e8f37a43	Sort VCs by alphabetical order	2022-04-04 17:51:41 +02:00
Denis Merigoux	84144c0a56	Tests now passing except for a few position and printing issues [skip ci]	2022-04-04 12:25:00 +02:00
Aymeric Fromherz	cca2e00d42	[Z3encoding] Add bad unit tests for duration	2022-03-24 17:27:03 +01:00
Aymeric Fromherz	55dd389819	[Z3encoding] Add good unit tests for duration	2022-03-24 17:23:31 +01:00
Aymeric Fromherz	cb36b9d72f	[Z3backend] Bad unit tests for EInj node	2022-03-16 12:04:31 +01:00
Aymeric Fromherz	d758170cde	[Z3backend] Good unit tests for EInj node	2022-03-16 12:03:24 +01:00
Aymeric Fromherz	bb57abf750	Negative tests for array length encoding	2022-03-16 11:23:36 +01:00
Aymeric Fromherz	123541dc34	Add positive test for array length	2022-03-16 11:21:54 +01:00
Aymeric Fromherz	f5a3a19a09	[Z3 encoding]: Add negative tests for rationals	2022-02-19 02:02:48 +01:00
Aymeric Fromherz	1dc1d6a3b8	Good test for rationals	2022-02-19 02:00:46 +01:00
Aymeric Fromherz	56e3720699	Add unit tests for TUnit	2022-02-17 18:42:22 +01:00
Denis Merigoux	e1dc36f1b1	Merge branch 'master' into io-qualifiers-112-part-2	2022-02-10 22:59:37 +01:00
Denis Merigoux	5004929a51	Fix #193 -- authored with @R1kM ... Moved no model generation flag Fixed bug for VC generation in the IfThenElse case	2022-02-10 16:49:01 +01:00
Denis Merigoux	2263dd7dab	Update syntax highlighting and test suite [skip ci]	2022-02-07 12:04:48 +01:00
Denis Merigoux	13b476d0a1	[skip ci] reorganized desugared to scope encoding, broke some invariants ... WIP: fixed some bugs and provided documentations but one thing missing	2022-01-28 17:31:31 +01:00
Denis Merigoux	5e253ba321	Disabling exact counterexamples values from CI testing because of randomness	2022-01-26 16:24:09 +01:00
Aymeric Fromherz	661b30f638	Add bad tests for date_get_year	2022-01-17 15:05:06 +01:00
Aymeric Fromherz	c7fd00702a	Fix good get year test + reset [skip ci]	2022-01-17 15:04:05 +01:00
Aymeric Fromherz	cf63e4f3d3	Restore pretty-printing of enum model [skip ci]	2022-01-14 21:10:34 +01:00
Aymeric Fromherz	271d20dcaf	todo outputs for bad struct tests [skip ci]	2022-01-14 20:42:06 +01:00
Aymeric Fromherz	ede73501d6	Add bad struct tests [skip ci]	2022-01-14 20:41:03 +01:00
Aymeric Fromherz	8b1c2d0891	reset test [skip ci]	2022-01-14 20:38:11 +01:00
Aymeric Fromherz	9684e14b1b	reset tests [skip ci]	2022-01-14 19:24:20 +01:00
Aymeric Fromherz	a128a188ee	reset [skip ci]	2022-01-14 19:05:58 +01:00
Aymeric Fromherz	9727acc788	more tests [skip ci]	2022-01-14 19:04:23 +01:00
Aymeric Fromherz	38b4912161	Reset test [skip ci]	2022-01-14 19:02:59 +01:00
Aymeric Fromherz	867fc46515	Add more complex enum test [skip ci]	2022-01-14 19:01:23 +01:00
Aymeric Fromherz	cc026e35b3	Add negative tests for enums	2022-01-14 18:37:32 +01:00
Aymeric Fromherz	d7563c229e	Reset test [skip ci]	2022-01-14 18:34:58 +01:00
Denis Merigoux	08591fd178	Add link to demo	2022-01-14 16:52:30 +01:00
Aymeric Fromherz	7ca0ca4012	Reset bad dates examples with expected outputs [skip ci]	2022-01-14 02:09:20 +01:00
Aymeric Fromherz	59e36d2750	Reset good dates simple test [skip ci]	2022-01-14 01:56:07 +01:00
Aymeric Fromherz	c8be75ca75	Z3encoding: Add bad tests related to dates [skip ci]	2022-01-13 20:28:28 +01:00
Aymeric Fromherz	52f33aa1ae	Fix good date example [skip ci]	2022-01-13 20:25:16 +01:00
Aymeric Fromherz	a6c88b103f	Reset bad money tests [skip ci]	2022-01-13 20:13:12 +01:00
Aymeric Fromherz	28935c689d	Reset good money test [skip ci]	2022-01-13 20:12:28 +01:00
Aymeric Fromherz	a15fb872ef	Fix money tests [skip ci]	2022-01-13 20:11:42 +01:00
Aymeric Fromherz	69e34b4ae7	Negative tests for money [skip ci]	2022-01-13 19:34:34 +01:00
Denis Merigoux	428ae95c62	[skip ci] Added a walkthrough example for ProLaLa + tweaked tests output order of vcs	2022-01-13 16:58:43 +01:00
Denis Merigoux	496775b148	Dates and money tests	2022-01-13 16:20:43 +01:00
Denis Merigoux	bf444f548f	Error message pretty-printing and sat solving example [skip ci]	2022-01-13 10:46:23 +01:00
Aymeric Fromherz	c0a8362fd9	[skip ci] Z3 encoding: update last missing examples with TODOs	2022-01-12 19:19:42 +01:00
Aymeric Fromherz	d6205369bb	[skip ci] reset bad proof tests	2022-01-12 19:09:50 +01:00
Aymeric Fromherz	ad974b16d6	[skip ci] reset bad proof test	2022-01-12 18:17:25 +01:00
Aymeric Fromherz	47032e058a	[skip ci] reset bad proof test	2022-01-12 18:16:46 +01:00
Aymeric Fromherz	1241f332d5	[skip ci] proof platform: functions good test now passing	2022-01-12 17:38:49 +01:00
Denis Merigoux	78b1fe08f4	[skip ci] Always name of the variable on the left	2022-01-12 16:56:05 +01:00
Denis Merigoux	6d06f9c81c	Prettified error messages	2022-01-12 16:50:10 +01:00
Aymeric Fromherz	5cb55e16fb	[skip ci] more minor test resets	2022-01-12 15:06:46 +01:00