diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index 0e589c0147a6f57654eb8dcd39b9bc8462121b9a..a435f36ad32a1082645d16cb1d8f4136c3588b6b 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -138,7 +138,7 @@ public class AvatarExpressionAttribute {
                     mask = 0xFF;
                 }
             } else {
-                accessIndex = SpecificationBlock.ATTR_INDEX + offset + ((attributeIndex - offset) / 32);
+                accessIndex = SpecificationBlock.ATTR_INDEX + (offset + optRatio - 1) / optRatio + ((attributeIndex - offset) / 32);
                 shift = (attributeIndex - offset) % 32;
                 mask = 1;
             }
@@ -180,7 +180,7 @@ public class AvatarExpressionAttribute {
                     mask = 0xFF;
                 }
             } else {
-                accessIndex = SpecificationBlock.ATTR_INDEX + offset + ((attributeIndex - offset) / 32);
+                accessIndex = SpecificationBlock.ATTR_INDEX + (offset + optRatio - 1) / optRatio + ((attributeIndex - offset) / 32);
                 shift = (attributeIndex - offset) % 32;
                 mask = 1;
             }
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index b11deecc674a9c5c0eb645b8bc524ab9e1d3ab31..deed36170ed4e3797cb4135961daa754ffa39129 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -432,6 +432,12 @@ public class AvatarSpecification extends AvatarElement {
             block.sortAttributes();
         }
     }
+    
+    public void setAttributeOptRatio(int attributeOptRatio) {
+        for(AvatarBlock block: blocks) {
+            block.setAttributeOptRatio(attributeOptRatio);
+        }
+    }
 //
 //    private void renameTimers() {
 //        // Check whether timers have the same name in different blocks
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index fa50768658b38fddda8026d33d9480fe639ab93c..744713c9e6457c803d3d28fb118e9b999d247511 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -736,6 +736,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         prepareStates();
         
         spec.sortAttributes();
+        spec.setAttributeOptRatio(2);
         initExpressionSolvers();
 
         prepareTransitions();
diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
index c73dc0d0ba3d12dc25729b6548240f820bb88e45..88c068afd1f461082cb9d2365a50ff0f7efc5864 100644
--- a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
+++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
@@ -181,6 +181,7 @@ public class AvatarExpressionTest {
     @Test
     public void testSpec() {
         as.sortAttributes();
+        as.setAttributeOptRatio(2);
         SpecificationState ss = new SpecificationState();
         ss.setInit(as, false);