Quantifier and Heap Reasoning Improvements - #3961

Open

unp1 wants to merge 17 commits into

mainfrom

bubel/quantifier-shape-fallback

Commits on Sep 1, 2026

Instantiate quantifiers over shifted array indices
unp1
committed
bc193a6
Make a quantified property applicable across a method call
unp1
committed
ece0673
If reading the value of two locations (o,f) and (u,f) has different values then o != u
unp1
committed
007ec71
Fix FilterStrategy approval check
unp1
committed
4ce7451
Separate the two halves of a theory's contribution to quantifier instantiation
unp1
committed
1203166
Restructure quantifier heuristics package
unp1
committed
eb43e80
Rework trigger selection around named values
unp1
committed
112b3a2
Enable improved quantification for affine shifted indices also for finite sequences
unp1
committed
62ad170
Generalize the heap of every read of the quantified variables inside a trigger
unp1
committed
1818a29
Carry an instance's origin and cost in one table
unp1
committed
d9b92de
Ask the theories for fallback triggers where a clause has none
unp1
committed
ac77848
State comment relations with exact verbs
unp1
committed
680242b
Record what trigger selection found per literal
unp1
committed
21eaee3
Ask for fallback triggers only where no clause of the formula is covered
unp1
committed
efae7fc
Formulas for which no triggers are generated may use equations from which to derive triggers (addresses issue #3972)
unp1
committed
29786fb
Add examples
unp1
committed
11331fc
Fix bug in OpReplacer
unp1
committed
decb5f1