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.