12 Commits

Author	SHA1	Message	Date
Patrick Lühne	8c801426a5	Allow U, V, and W for program variables	2020-06-05 18:50:09 +02:00
Patrick Lühne	27fff47c91	Minor refactoring	2020-05-29 18:42:14 +02:00
Patrick Lühne	fc34aadf90	Show all predicates used in specification by default	2020-05-29 18:41:16 +02:00
Patrick Lühne	93db8d02b5	Implement tightness check	2020-05-29 14:57:00 +02:00
Patrick Lühne	e57a1859d2	Fix supertightness check	2020-05-28 18:37:34 +02:00
Patrick Lühne	870fdd048c	Handle input predicates correctly	2020-05-28 06:29:57 +02:00
Patrick Lühne	491a255811	Require supertight programs for backward proof	2020-05-28 05:03:56 +02:00
Patrick Lühne	9b7895a032	Don’t append variable ID if there is only one	2020-05-22 19:43:41 +02:00
Patrick Lühne	116f74f63e	Minor clean-up	2020-05-22 18:17:00 +02:00
Patrick Lühne	81ddfd450a	Use custom foliage flavor ... With this patch, properties specific to variable, function, and predicate declarations are directly stored within those objects rather than external maps that need to be queried via traits. This greatly simplifies many parts of the logic. This is made possible by implementing a custom foliage flavor, which makes it possible to swap the built-in declaration types for extended versions of those types that fulfill certain requirements.	2020-05-22 02:25:00 +02:00
Patrick Lühne	c3860c1bf1	Check variable declaration stack before using it	2020-02-09 10:22:08 +07:00
Patrick Lühne	a7e8368634	Work in progress	2020-01-24 13:32:43 +01:00