As can be seen from the latest comp.out file, the circuits and netlists now match uniquely. However, it shows some property errors.