uwdb / Cosette

Cosette is an automated SQL solver.
BSD 2-Clause "Simplified" License
666 stars 54 forks source link

incorrect coq code gen when constant in aggregate expr #50

Closed stechu closed 7 years ago

stechu commented 7 years ago
-- define schema r with attributes a and b
schema s(a:int, b:int); 

table r(s);            -- define table r using schema s

query q1                -- define query q1 
`select sum(1+x.b) 
 from r x`;

query q2                -- define query q2 likewise
`select sum(1+y.b) 
 from r y`;

verify q1 q2;           -- does q1 equal to q2?

generate incorrect coq code.