/* define schema employee,
here employee can contain any number of attributes,
but it has to at least contain integer attributes
eid and age */
schema customer(id:int, name:text, city:text);
schema account(num:int, branch:text, custid:int, balance:int);
-- define table uw_emp using schema s1
table accs(account);
-- define table uw_sal using schema s1
table custs(customer);
-- define query q1 over uw_emp and uw_payroll
query q1
`select c.id, c.name
from accs a, custs c
where c.id=a.custid
and a.balance = (select max(al.balance) from accs as al)
group by c.id, c.name`;
-- define query q2 likewise
query q2
`select distinct c.id, c.name
from accs a, custs c
where c.id=a.custid
and a.balance = (select max(al.balance) from accs as al)
`;
verify q1 q2; -- does q1 equal to q2?
results in
Coq and Rosette executions doesn't agree. File an issue!
results in