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