Can't verify queries with const expr

[zedware]

/* define schema s1,
here s1 can contain any number of attributes,
but it has to at least contain integer attributes
x and y */
schema s1(x:int, y:int, ??);

table a(s1); -- table a of schema s1

query q1 -- query 1
select x.x as ax from a x where 1=1;

query q2 -- query 2
select x.x as ax from a x where 0=0;

verify q1 q2; -- verify the equivalence

[stechu]

@zedware which result did you get? I assume it is UNKNOWN?

[zedware]

Result
Two queries' equivalence is unknown.
Solver runs out of time.

[stechu]

@zedware thank you! this is a known issue. currently we don't interpret predicate. We are working on Cosette 2.0 that will fix this issue.