Repository navigation

Add exact summaries for pointwise loops behind --functionalize-loops - #852

Open

shaobo-he wants to merge 6 commits into

functionalize-loops

Open

Add exact summaries for pointwise loops behind --functionalize-loops#852
shaobo-he wants to merge 6 commits into
developfrom
functionalize-loops

Commits on Aug 26, 2026
- Add exact summaries for pointwise loops behind --functionalize-loops
  
  shaobo-he
  and
  claude
  committed
  32d25f9
- Emit loop summary maps as lifted functions, not lambda expressions
  
  shaobo-he
  and
  claude
  committed
  c91a4c3
- Leave the default translation untouched when loops are not functionalized
  
  shaobo-he
  and
  claude
  committed
  3eec7cf
- Run the functionalized-loop regressions through Corral as well
  
  shaobo-he
  and
  claude
  committed
  8eea174
- Run the functionalized-loop regressions in CI
  
  shaobo-he
  and
  claude
  committed
  6a36f85
- Make the loop summaries agree with SMACK's own lowering
  
  shaobo-he
  and
  claude
  committed
  1f72580