log/arrayeqerr1.btor:3: operands have different sort