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