Florian Hahn 0bcfd4cbac [ConstraintElimination] Rewrite tests to reduce verification complexity. ... This patch reduces the bitwidth of types certain tests operate and gets rid of a number of @use(i1) calls and xor's the conditions together instead, which eliminates all timeouts when verifying the tests. See https://github.com/AliveToolkit/alive2/issues/744 for more details.		2021-08-26 16:41:40 +01:00
..
add-nuw.ll	…
add.ll	…
and.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
assumes.ll	[ConstraintElimination] Initial support for using info from assumes.	2021-08-26 10:08:00 +01:00
decompose-with-temporary-indices.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
dom.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
empty-constraint.ll	…
eq.ll	…
gep-arithmetic.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
geps-inbounds-precondition.ll	[ConstraintElimination] Add gep tests without inbounds.	2021-03-22 12:23:30 +00:00
geps-pointers-to-arrays.ll	[ConstraintElimination] Add multi-dimension GEP tests.	2021-03-22 10:37:12 +00:00
geps-pointers-to-structs.ll	[ConstraintElimination] Add multi-dimension GEP tests.	2021-03-22 10:37:12 +00:00
geps-precondition-overflow-check.ll	[ConstraintElimination] Add gep tests without inbounds.	2021-03-22 12:23:30 +00:00
geps.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
i128.ll	…
large-system-growth.ll	…
loops-bottom-tested-base.ll	…
loops-bottom-tested-pointer-cmps.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
loops-header-tested-base.ll	…
loops-header-tested-pointer-cmps.ll	…
loops-header-tested-pointer-iv.ll	…
loops.ll	…
mixed-signed-unsigned-predicates.ll	…
mixed.ll	…
ne.ll	[ConstraintElimination] Use unsigned > 0 instead of != 0.	2021-02-22 17:54:36 +00:00
or.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
pointercast.ll	[ConstraintElimination] Only strip casts preserving the representation.	2021-03-26 20:07:41 +00:00
sge.ll	…
sub-nuw.ll	…
sub.ll	…
uge.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
ugt-ule.ll	…
ule.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00
vector-compares.ll	…
wrapping-math.ll	…
zext.ll	[ConstraintElimination] Rewrite tests to reduce verification complexity.	2021-08-26 16:41:40 +01:00