[WIP] Quantifier eleminiation work#8904

Draft

tautschnig wants to merge 28 commits intodiffblue:developfrom

tautschnig:quantifiers-backup

Commits on Feb 25, 2026

Eager quantifier elimination: support empty ranges

tautschnig
and
kiro-agent
committed
Quantifier instantiation via simplistic E-matching

tautschnig
and
kiro-agent
committed
Complete instantiation for quantifier elimination with offsets

tautschnig
and
kiro-agent
committed
Regression tests for complete quantifier instantiation

tautschnig
and
kiro-agent
committed
Set 20-minute timeout for all CMake-based regression tests

tautschnig
and
kiro-agent
committed
Add per-test timeout support (-t) to test.pl

tautschnig
and
kiro-agent
committed

Commits on Feb 26, 2026

Commits on Feb 27, 2026

Commits on Feb 28, 2026

Prefer Ye/de Moura complete instantiation over eager full-range for large arrays

kiro-agent
authored and
tautschnig
committed
Clean up Ye/de Moura instantiation: remove duplicate fallback and SSA check

kiro-agent
authored and
tautschnig
committed

Commits on Mar 3, 2026

Filter non-ground terms and ensure complete indices in quantifier instantiation

kiro-agent
authored and
tautschnig
committed