Incorrect result for RegLan comparison

[jurajsic]

For the following formula, ostrich (both latest commit and version 1.4) returns sat.
However, I believe it is unsat. The formula asks if an equation of empty language with an intersection of two concatenations holds. I think that the intersection is non-empty, it contains the word "iaqdjapypvaxcvhckgvyqagyaewwfatpaczdwzarcelwaprtlasaaaxckjgsmqjnaimkiaaaaspuivjiabezpemvmdpdjotyhxybmafinnsyregnaysdtzmncwyhslinghydkaaxiwjuaatyasvrsafqylofantetbxzfnvqlalozdlosfekaarftqwtagcoialpjgcqxcangebzankzadwxhvfzvnplahtmqabhtyxaadwuxybnkzsrxpadeptjdjbekaaxrdhgsikzgaaagmwyrbotwdatxalcmblaaalaaamvrianoiatqmsmpzlaaqmgtrholowanaahaqamslsoomxfdrlklsipanavajrepluugy"

wildcard-matching-regex-75.txt

[pruemmer]

Thanks for the bug report. You are right, the equation is unsat, but that is because SMT-LIB says that the sort RegLan is interpreted with ground regular expressions. That should mean that every regular expression evaluates to itself, and that two regular expressions are equal iff they are identical. Ostrich currently just considers the regex functions as uninterpreted functions.