Cosette icon indicating copy to clipboard operation
Cosette copied to clipboard

Equivalent queries with conditions on a date column generate invalid Coq code

Open milos-simic opened this issue 4 years ago • 0 comments

This code:

schema student_schema(indeks:int, ime:varchar, prezime:varchar, datum_upisa:date, datum_rodjenja:date, mesto_rodjenja:varchar);
schema predmet_schema(id_predmeta:int, shifra:char, naziv:varchar, bodovi:int);
schema ispitni_rok_schema(godina_roka:int, oznaka_roka:char, naziv:varchar);
schema ispit_schema(indeks:int, id_predmeta:int, godina_roka:int, oznaka_roka:char, ocena:int, datum_ispita:date, bodovi:int);

table student(student_schema);
table predmet(predmet_schema);
table ispitni_rok(ispitni_rok_schema);
table ispit(ispit_schema);

query q1 
`SELECT DISTINCT s.* FROM student s WHERE s.datum_rodjenja='2014-7-1'`;

query q2
`select distinct s.* from student s where s.datum_rodjenja = '2014-7-1'`;

verify q1 q2;

returns this message: Invalid generated Coq code. Please file an issue.

When I changed the condition to s.indeks=1, the two queries were correctly recognized as equivalent to one another.

I thought that maybe the date should be formatted so that the month and day have leading zeroes, so I changed '2014-7-1' to '2014-07-01', but the error was still there.

milos-simic avatar Sep 05 '19 22:09 milos-simic