Exactly Equal Queries Time out

[Njanderson]

The following queries are not known as equivalent, even though they are exactly the same. Maybe you could try sorting the x = y and y = x, such that they are all x = y or something. Either way, I feel like it should know that these are equivalent statements.

schema sch_flights(fid:int,
    year:int,
    month_id:int,
    day_of_month:int,
    day_of_week_id:int,
    carrier_id:string,
    flight_num:int,
    origin_city:string,
    origin_state:string,
    dest_city:string,
    dest_state:string,
    departure_delay:int,
    taxi_out:int,
    arrival_delay:int,
    canceled:int,
    actual_time:int,
    distance:int,
    capacity:int,
    price:int
);

schema sch_carriers
(
    cid:int,
    name:string
);

SCHEMA sch_months
(
    mid:int,
    month:string
);

SCHEMA sch_days
(
    did:int,
    day_of_week:string
);

table Flights(sch_flights);
table Carriers(sch_carriers);
table Weekdays(sch_days);
table Months(sch_months);
query q1                -- define query q1 on tables a and b
` select C.name as name, sum(F.departure_delay) as delay
 from FLIGHTS as F, CARRIERS as C
 where C.cid=F.carrier_id 
 group by F.carrier_id`;

query q2                -- define query q2 likewise
`select c.name as name, sum(f.departure_delay) as delay
from FLIGHTS as f, CARRIERS as c
where f.carrier_id = c.cid
group by f.carrier_id`;

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

[stechu]

Thanks! @Njanderson That's one of the known problems. We will fix this in the next version. Unfortunately, it will take some time.
One thing that may help is, I would like to change UNKNOWN to LIKELY EQ. Since it is acutally bounded model checking, 99.9 % UNKNOWN now is actually equal.