Replace zero registers in specifications

Signed-off-by: Hernan Ponce de Leon <[email protected]>

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java

@@ -94,21 +94,22 @@ public Program build() {
     The zero register plays a special role in some architectures:
       1. Reading accesses always return the value 0.
       2. Discards data when written.
-     TODO: The below code is a simple fix to guarantee point 1. above.
-      Point 2. might also be resolved: although we do not prevent writing to xzr,
-      the value of xzr is never read after the transformation so its value is effectively 0.
-      However, the exists/forall clauses could still refer to that register and observe a non-zero value.
-     */
+    TODO: The below code is a simple fix to guarantee point 1. above.
+    Point 2. might also be resolved: although we do not prevent writing to the zero register,
+    its value is never read after the transformation so its value is effectively 0.
+    */
     private void replaceZeroRegister() {
         if(zeroRegister != null) {
-            final ExpressionVisitor<Expression> xzrReplacer = new ExprTransformer() {
+            final ExpressionVisitor<Expression> zeroRegReplacer = new ExprTransformer() {
                 @Override
                 public Expression visitRegister(Register reg) {
                     return reg.getName().equals(zeroRegister) ? expressions.makeGeneralZero(reg.getType()) : reg;
                 }
             };
             program.getThreadEvents(RegReader.class)
-                    .forEach(e -> e.transformExpressions(xzrReplacer));
+                    .forEach(e -> e.transformExpressions(zeroRegReplacer));
+            program.setSpecification(program.getSpecificationType(),
+                    program.getSpecification().accept(zeroRegReplacer));
         }
     }