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.