diff --git a/Gillian-JS/Examples/Amazon/AmazonLogic.jsil b/Gillian-JS/Examples/Amazon/AmazonLogic.jsil
index b666fb26..00613afe 100644
--- a/Gillian-JS/Examples/Amazon/AmazonLogic.jsil
+++ b/Gillian-JS/Examples/Amazon/AmazonLogic.jsil
@@ -37,7 +37,6 @@ lemma ObjectTableAbsentProperty(l, PVPairs, prop)
     ((#l, #prop) -> none) *
     empty_fields(#l : -u- (#pSet, -{ #prop }-))
 ]]
-[*  *]
 
 (* Removing a property from a list of prop-value pairs *)
 pred RemoveProp(+PVPairs : List, +prop : Str, found : Bool, value : Str, newPairs : List) :
diff --git a/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil b/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil
index a6242072..90749448 100644
--- a/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil
+++ b/Gillian-JS/Examples/Amazon/EncryptionHeaderLogic.gil
@@ -15,11 +15,12 @@
                 readPos
 *)
 pred Field(+buffer : List, +readPos : Num, field : List, length : Num) :
-  (0 <=# readPos) * (#rawFL == l-sub(buffer, readPos, 2)) *
+  (0 <=# readPos) * (is_int readPos) *
+    (#rawFL == l-sub(buffer, as_int readPos, 2i)) *
     rawToUInt16(#rawFL, false, #fLength) *
-    (field == l-sub(buffer, (readPos + 2), #fLength)) *
-    (length == (2 + #fLength)) * ((readPos + length) <=# (l-len buffer));
-  facts: (2 <=# length);
+    (field == l-sub(buffer, as_int (readPos + 2), as_int #fLength)) *
+    (length == (2 + #fLength)) * ((readPos + length) <=# as_num (l-len buffer));
+  facts: (2 <=# length) and (is_int readPos) and (is_int length);
 
 
 (****************************
@@ -43,7 +44,7 @@ pred Field(+buffer : List, +readPos : Num, field : List, length : Num) :
 *)
 @nopath
 pred CElement(+buffer : List, +readPos : Num, +fCount : Num, element : List, length : Num) :
-  (0 <=# readPos) * (readPos <=# (l-len buffer)) *
+  (0 <=# readPos) * (readPos <=# as_num (l-len buffer)) *
     (fCount == 0) * (element == {{  }}) * (length == 0),
   (0 <# fCount) * Field(buffer, readPos, #field, #fLength) *
     (#restFCount == (fCount - 1)) *
@@ -53,7 +54,10 @@ pred CElement(+buffer : List, +readPos : Num, +fCount : Num, element : List, len
       A complete element has a non-negative number of fields
       and length, and must be correctly positioned within a buffer
   *)
-  facts: (0 <=# readPos) and (0 <=# fCount) and (0 <=# length) and ((readPos + length) <=# (l-len buffer)) and ((l-len element) == fCount);
+  facts: (0 <=# readPos) and (0 <=# fCount) and (0 <=# length) and
+         ((readPos + length) <=# as_num (l-len buffer)) and
+         (l-len element == as_int fCount) and
+         (is_int readPos) and (is_int fCount) and (is_int length);
 
 (* The length of an element is not smaller than the length of its first field *)
 lemma CElementFirstFieldLength(buffer, readPos, fCount, field, restFields, eLength)
@@ -62,7 +66,7 @@ lemma CElementFirstFieldLength(buffer, readPos, fCount, field, restFields, eLeng
 ]]
 [[
     CElement(#buffer, #readPos, #fCount, l+({{ #field }}, #restFields), #eLength) *
-    (2 + l-len #field <=# #eLength)
+    (2 + as_num (l-len #field) <=# #eLength)
 ]]
 [*
     unfold CElement(#buffer, #readPos, #fCount, l+({{ #field }}, #restFields), #eLength)
@@ -88,7 +92,7 @@ lemma AppendFieldCC(buffer, readPos, fCount1, fList1, eLength1, fCount2, field,
 [[
     CElement(#buffer, #readPos, #fCount1, #fList1, #eLength1) *
     CElement(#buffer, #readPos + #eLength1, #fCount2, l+({{ #field }}, #fList2), #eLength2) *
-    (#shift == 2 + l-len #field)
+    (#shift == 2 + as_num (l-len #field))
 ]]
 [[
     CElement(#buffer, #readPos, #fCount1 + 1, l+ (#fList1, {{ #field }}), #eLength1 + #shift) *
@@ -99,9 +103,10 @@ lemma AppendFieldCC(buffer, readPos, fCount1, fList1, eLength1, fCount2, field,
     unfold CElement(#buffer, #readPos, #fCount1, #fList1, #eLength1);
     if (0 < #fCount1) then {
         sep_assert ((#fList1 == l+ ({{ #fl1 }}, #rfl1))) [bind: #fl1, #rfl1];
-        sep_assert (CElement(#buffer, 2 + (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1)) [bind: #reL1];
-        apply AppendFieldCC(#buffer, 2 + (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1, #fCount2, #field, #fList2, #eLength2)
-    }
+        sep_assert (CElement(#buffer, 2 + (as_num (l-len #fl1)) + #readPos, #fCount1 - 1, #rfl1, #reL1)) [bind: #reL1];
+        apply AppendFieldCC(#buffer, 2 + (as_num (l-len #fl1)) + #readPos, #fCount1 - 1, #rfl1, #reL1, #fCount2, #field, #fList2, #eLength2)
+    };
+    fold CElement(#buffer, #readPos, #fCount1 + 1, l+ (#fList1, {{ #field }}), #eLength1 + #shift)
 *]
 
 (****************************
@@ -125,7 +130,7 @@ lemma AppendFieldCC(buffer, readPos, fCount1, fList1, eLength1, fCount2, field,
 *)
 pred CElements(+buffer : List, +readPos : Num, +eCount : Num, +fCount : Num,
                elements : List, length : Num) :
-  (0 <=# readPos) * (readPos <=# (l-len buffer)) * (eCount == 0) *
+  (0 <=# readPos) * (readPos <=# as_num (l-len buffer)) * (eCount == 0) *
   (0 <# fCount) * (elements == {{  }}) * (length == 0),
   (0 <=# readPos) * (0 <# eCount) * (0 <# fCount) * (0 <# length) *
     CElement(buffer, readPos, fCount, #element, #eLength) * (#restECount == (eCount - 1)) *
@@ -139,7 +144,11 @@ pred CElements(+buffer : List, +readPos : Num, +eCount : Num, +fCount : Num,
       correctly positioned within a buffer
   *)
   facts: (0 <=# readPos) and (0 <=# eCount) and (0 <# fCount) and (0 <=# length) and
-         ((readPos + length) <=# (l-len buffer)) and (eCount == (l-len elements));
+         ((readPos + length) <=# as_num (l-len buffer)) and (as_int eCount == l-len elements) and
+         (is_int readPos) and
+         (is_int eCount) and
+         (is_int fCount) and
+         (is_int length);
 
 (* Appending a complete element to the given complete elements from the right *)
 lemma CElementsAppend(buffer, readPos, eCount, fCount, eList, esLength, fList, eLength)
@@ -168,7 +177,7 @@ lemma CElementsElementLength(buffer, readPos, eCount, fCount, eList, prefix, ele
 ]]
 [[
     CElements(#buffer, #readPos, #eCount, #fCount, #eList, #esLength) *
-    (l-len #element == #fCount)
+    (l-len #element == as_int #fCount)
 ]]
 [*
     apply DestructList(#prefix);
@@ -178,7 +187,8 @@ lemma CElementsElementLength(buffer, readPos, eCount, fCount, eList, prefix, ele
         sep_assert ((#prefix == l+ ({{ #head }}, #rest))) [bind: #head, #rest];
         sep_assert (CElements(#buffer, (#readPos + #elementLength), (#eCount - 1), #fCount, l+ (#rest, {{#element}}, #suffix), #restESLength)) [bind: #restESLength];
         apply CElementsElementLength(#buffer, (#readPos + #elementLength), (#eCount - 1), #fCount, l+ (#rest, {{#element}}, #suffix), #rest, #element, #suffix)
-    }
+    };
+    fold CElements(#buffer, #readPos, #eCount, #fCount, #eList, #esLength)
  *]
 
 (******************************
@@ -224,19 +234,19 @@ lemma CElementsElementLength(buffer, readPos, eCount, fCount, eList, prefix, ele
 @nopath
 pred IElement(+buffer : List, +readPos : Num, +fCount : Num, fList : List, eLength : Num) :
   (* Base case: not enough data to read length of next field *)
-  (0 <=# readPos) * (0 <# fCount) * (readPos <=# (l-len buffer)) *
-    ((l-len buffer) <# (readPos + 2)) * (fList == {{  }}) *
-    (eLength == ((l-len buffer) - readPos)),
+  (0 <=# readPos) * (0 <# fCount) * (readPos <=# as_num (l-len buffer)) *
+    (as_num (l-len buffer) <# (readPos + 2)) * (fList == {{  }}) *
+    (eLength == ((as_num (l-len buffer)) - readPos)),
 
   (* Base case: enough data to read length of next field, but not enough data to read next field *)
-  (0 <=# readPos) * (0 <# fCount) * ((readPos + 2) <=# (l-len buffer)) *
-    (#rawFL == l-sub(buffer, readPos, 2)) * rawToUInt16(#rawFL, false, #fLength) *
-    ((l-len buffer) <# ((readPos + 2) + #fLength)) * (fList == {{  }}) *
-    (eLength == ((l-len buffer) - (readPos + 2))),
+  (0 <=# readPos) * (0 <# fCount) * ((readPos + 2) <=# as_num (l-len buffer)) *
+    (#rawFL == l-sub(buffer, as_int readPos, 2i)) * rawToUInt16(#rawFL, false, #fLength) *
+    (as_num (l-len buffer) <# ((readPos + 2) + #fLength)) * (fList == {{  }}) *
+    (eLength == ((as_num (l-len buffer)) - (readPos + 2))),
 
   (* Recursive case: enough data to read one field, but not enough data to read the remaining ones *)
   (0 <=# readPos) * (1 <# fCount) * Field(buffer, readPos, #field, #fLength) *
-    (#restFCount == (fCount - 1)) * ((readPos + #fLength) <=# (l-len buffer)) *
+    (#restFCount == (fCount - 1)) * ((readPos + #fLength) <=# as_num (l-len buffer)) *
     IElement(buffer, (readPos + #fLength), #restFCount, #restFList, #restELength) *
     (fList == l+ ({{ #field }}, #restFList)) *
     (eLength == (#fLength + #restELength));
@@ -245,14 +255,15 @@ pred IElement(+buffer : List, +readPos : Num, +fCount : Num, fList : List, eLeng
         An incomplete element must have a strictly positive number of fields,
         non-negative length, and must fit within the buffer
     *)
-  facts: (0 <=# readPos) and (readPos <=# (l-len buffer)) and (0 <# fCount) and (0 <=# eLength);
+  facts: (0 <=# readPos) and (readPos <=# as_num (l-len buffer)) and (0 <# fCount) and (0 <=# eLength) and
+         (is_int readPos) and (is_int fCount) and (is_int eLength);
 
 (* Appending the first field of a given incomplete element to a complete element on its left *)
 lemma AppendFieldCI(buffer, readPos, fCount1, fList1, eLength1, fCount2, field, fList2, eLength2)
 [[
     CElement(#buffer, #readPos, #fCount1, #fList1, #eLength1) *
     IElement(#buffer, #readPos + #eLength1, #fCount2, l+({{ #field }}, #fList2), #eLength2) *
-    (#shift == 2 + l-len #field)
+    (#shift == 2 + as_num (l-len #field))
 ]]
 [[
     CElement(#buffer, #readPos, #fCount1 + 1, l+ (#fList1, {{ #field }}), #eLength1 + #shift) *
@@ -262,9 +273,10 @@ lemma AppendFieldCI(buffer, readPos, fCount1, fList1, eLength1, fCount2, field,
     unfold CElement(#buffer, #readPos, #fCount1, #fList1, #eLength1);
     if (0 < #fCount1) then {
         sep_assert ((#fList1 == l+ ({{ #fl1 }}, #rfl1))) [bind: #fl1, #rfl1];
-        sep_assert (CElement(#buffer, 2 + (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1)) [bind: #reL1];
-        apply AppendFieldCI(#buffer, 2 + (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1, #fCount2, #field, #fList2, #eLength2)
-    }
+        sep_assert (CElement(#buffer, 2 + as_num (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1)) [bind: #reL1];
+        apply AppendFieldCI(#buffer, 2 + as_num (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1, #fCount2, #field, #fList2, #eLength2)
+    };
+    fold CElement(#buffer, #readPos, #fCount1 + 1, l+ (#fList1, {{ #field }}), #eLength1 + #shift)
 *]
 
 (* Prepend an entire complete element to an incomplete element following it *)
@@ -280,8 +292,8 @@ lemma PrependCElementI(buffer, readPos, fCount1, fList1, eLength1, fCount2, fLis
     unfold CElement(#buffer, #readPos, #fCount1, #fList1, #eLength1);
     if (0 < #fCount1) then {
         sep_assert ((#fList1 == l+ ({{ #fl1 }}, #rfl1))) [bind: #fl1, #rfl1];
-        sep_assert (CElement(#buffer, 2 + (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1)) [bind: #reL1];
-        apply PrependCElementI(#buffer, 2 + (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1, #fCount2, #fList2, #eLength2)
+        sep_assert (CElement(#buffer, 2 + as_num (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1)) [bind: #reL1];
+        apply PrependCElementI(#buffer, 2 + as_num (l-len #fl1) + #readPos, #fCount1 - 1, #rfl1, #reL1, #fCount2, #fList2, #eLength2)
     }
 *]
 
@@ -320,16 +332,17 @@ lemma PrependCElementI(buffer, readPos, fCount1, fList1, eLength1, fCount2, fLis
 pred IElements(+buffer : List, +readPos : Num, +eCount : Num, +fCount : Num,
                eList : List, esLength : Num) :
   (* Base case: single incomplete element *)
-  (0 <=# readPos) * (readPos <=# (l-len buffer)) * (0 <# eCount) * (0 <# fCount) *
+  (0 <=# readPos) * (readPos <=# as_num (l-len buffer)) * (0 <# eCount) * (0 <# fCount) *
     IElement(buffer, readPos, fCount, #fList, esLength) * (eList == {{  }}),
 
   (* Recursive case: enough data to read first element, but not enough data to read the remaining ones *)
-  (0 <=# readPos) * (readPos <=# (l-len buffer)) * (1 <# eCount) * (0 <# fCount) *
+  (0 <=# readPos) * (readPos <=# as_num (l-len buffer)) * (1 <# eCount) * (0 <# fCount) *
     CElement(buffer, readPos, fCount, #fList, #eLength) *
     (#restECount == (eCount - 1)) *
     IElements(buffer, (readPos + #eLength), #restECount, fCount, #restEList, #restESLength) *
     (eList == l+ ({{ #fList }}, #restEList)) * (esLength == (#eLength + #restESLength));
-  facts: (0 <=# readPos) and (readPos <=# (l-len buffer)) and (0 <# eCount) and (0 <# fCount) and (0 <=# esLength);
+  facts: (0 <=# readPos) and (readPos <=# as_num (l-len buffer)) and (0 <# eCount) and (0 <# fCount) and (0 <=# esLength) and
+         (is_int readPos) and (is_int eCount) and (is_int fCount) and (is_int esLength);
 
 
 
@@ -350,7 +363,8 @@ nounfold pred Elements(definition : Str, +buffer : List, +readPos : Num,
                        esLength : Num) :
   (definition == "Complete") * CElements(buffer, readPos, eCount, fCount, eList, esLength),
   (definition == "Incomplete") * IElements(buffer, readPos, eCount, fCount, eList, esLength);
-  facts: (0 <=# readPos) and (readPos <=# (l-len buffer)) and (0 <=# eCount) and (0 <# fCount) and (0 <=# esLength);
+  facts: (0 <=# readPos) and (readPos <=# as_num (l-len buffer)) and (0 <=# eCount) and (0 <# fCount) and (0 <=# esLength) and
+         (is_int readPos) and (is_int eCount) and (is_int fCount) and (is_int esLength);
 
  (* An entire complete element sequence can be prepended to a general element sequence *)
 lemma PrependCElementsE(definition, buffer, readPos, eCount1, fCount, fList1, esLength1, eCount2, fList2, esLength2)
@@ -367,7 +381,7 @@ lemma PrependCElementsE(definition, buffer, readPos, eCount1, fCount, fList1, es
     if (0 < #eCount1) then {
         apply PrependCElementsE(#definition, #buffer, #readPos + #eLength, #eCount1 - 1, #fCount, #restElements, #restESLength, #eCount2, #fList2, #esLength2);
         unfold Elements(#definition, #buffer, (#eLength + #readPos), ((-1. + #eCount1) + #eCount2), #fCount, l+ (#restElements, #fList2), (#restESLength + #esLength2));
-        if (definition == "Incomplete") then {
+        if (#definition == "Incomplete") then {
             fold IElements(#buffer, #readPos, #eCount1 + #eCount2, #fCount, l+ (#fList1, #fList2), #esLength1 + #esLength2)
         }
     }
@@ -396,8 +410,8 @@ lemma PrependCElementsE(definition, buffer, readPos, eCount1, fCount, fList1, es
 @nopath
 nounfold pred CRawEncryptedDataKeys(+buffer : List, +readPos : Num,
                                     EDKs : List, EDKsLength : Num) :
-    (0 <=# readPos) * (readPos <=# (l-len buffer)) *
-    (#rawEC == l-sub(buffer, readPos, 2)) *
+    (0 <=# readPos) * (readPos <=# as_num (l-len buffer)) *
+    (#rawEC == l-sub(buffer, as_int readPos, 2i)) *
     rawToUInt16(#rawEC, false, #keyCount) * (0 <# #keyCount) *
     Elements("Complete", buffer, (readPos + 2), #keyCount, 3, EDKs, #EDKsLength) *
     (EDKsLength == (#EDKsLength + 2));
@@ -406,25 +420,28 @@ nounfold pred CRawEncryptedDataKeys(+buffer : List, +readPos : Num,
 @nopath
 nounfold pred IRawEncryptedDataKeys(buffer : List, readPos : Num) :
   (* Not enough data to read the number of EDKs *)
-  (0 <=# readPos) * (readPos <=# (l-len buffer)) * ((l-len buffer) <# (readPos + 2)),
+  (is_int readPos) * (0 <=# readPos) * (readPos <=# as_num (l-len buffer)) * (as_num (l-len buffer) <# (readPos + 2)),
 
-    (* Enough data to read the number of EDKs, but not enough data to read the EDKs *)
-  (0 <=# readPos) * ((readPos + 2) <=# (l-len buffer)) * (#rawEC == l-sub(buffer, readPos, 2)) *
+  (* Enough data to read the number of EDKs, but not enough data to read the EDKs *)
+  (is_int readPos) * (0 <=# readPos) * ((readPos + 2) <=# as_num (l-len buffer)) * (#rawEC == l-sub(buffer, as_int readPos, 2i)) *
     rawToUInt16(#rawEC, false, #keyCount) * (0 <# #keyCount) *
     Elements("Incomplete", buffer, (readPos + 2), #keyCount, 3, #eList, #esLength);
+  facts: (is_int readPos);
 
 (* Broken serialised EDKs *)
 @nopath
 nounfold pred BRawEncryptedDataKeys(errorMessage : Str, +buffer : List, +readPos : Num) :
   (* Incorrect starting position *)
-  ((readPos <# 0) \/ ((l-len buffer) <# readPos)) *
+  (is_int readPos) * ((readPos <# 0) \/ (as_num (l-len buffer) <# readPos)) *
     (errorMessage == "deserializeMessageHeader: startPos out of bounds."),
 
   (* Zero EDKs provided *)
-  (0 <=# readPos) * ((readPos + 2) <=# (l-len buffer)) *
-    (#rawEC == l-sub(buffer, readPos, 2)) * rawToUInt16(#rawEC, false, 0) *
+  (is_int readPos) * (0 <=# readPos) * ((readPos + 2) <=# as_num (l-len buffer)) *
+    (#rawEC == l-sub(buffer, as_int readPos, 2i)) * rawToUInt16(#rawEC, false, 0.) *
     (errorMessage == "Malformed Header: No EncryptedDataKey found.");
 
+  facts: (is_int readPos);
+
 (* General serialised EDKs *)
 @nopath
 nounfold pred RawEncryptedDataKeys(definition : Str, +buffer : List, +readPos : Num, EDKs : List, EDKsLength : Num, errorMessage : Str) :
@@ -454,41 +471,41 @@ nounfold pred RawEncryptedDataKeys(definition : Str, +buffer : List, +readPos :
 (* Complete serialised encryption context *)
 @nopath
 nounfold pred CRawEncryptionContext(+buffer : List, ECKs : List) :
-  ((l-len buffer) == 0) * (ECKs == {{  }}),
-  (#rawKC == l-sub(buffer, 0, 2)) *
+  ((l-len buffer) == 0i) * (ECKs == {{  }}),
+  (#rawKC == l-sub(buffer, 0i, 2i)) *
     rawToUInt16(#rawKC, false, #keyCount) * (0 <# #keyCount) *
     Elements("Complete", buffer, 2, #keyCount, 2, ECKs, #ECKsLength) *
     toUtf8PairMap(ECKs, #utf8ECKs) * FirstProj(ECKs, #ECKeys) *
-    Unique(#ECKeys) * ((2 + #ECKsLength) == (l-len buffer));
+    Unique(#ECKeys) * (as_int (2 + #ECKsLength) == (l-len buffer));
 
 (* Broken serialised encryption context *)
 @nopath
 nounfold pred BRawEncryptionContext(errorMessage:Str, +buffer:List, ECKs:List) :
     (* Not enough data provided *)
-    (2 <# l-len buffer) *
-    (#rawKC == l-sub (buffer, 0, 2)) *
+    (2i i<# (l-len buffer)) *
+    (#rawKC == l-sub (buffer, 0i, 2i)) *
     rawToUInt16(#rawKC, false, #keyCount) *
     (0 <# #keyCount) * (ECKs == {{ }}) *
     Elements("Incomplete", buffer, 2, #keyCount, 2, #eList, #esLength) *
     (errorMessage == "decodeEncryptionContext: Underflow, not enough data."),
 
     (* Too much data provided *)
-    (2 <# l-len buffer) *
-    (#rawKC == l-sub (buffer, 0, 2)) *
+    (2i <# (l-len buffer)) *
+    (#rawKC == l-sub (buffer, 0i, 2i)) *
     rawToUInt16(#rawKC, false, #keyCount) *
     (0 <# #keyCount) *
     Elements("Complete", buffer, 2, #keyCount, 2, ECKs, #ECKsLength) *
-    (! (#ECKsLength + 2 == l-len buffer)) *
+    (! (as_int (#ECKsLength + 2) == l-len buffer)) *
     (errorMessage == "decodeEncryptionContext: Overflow, too much data."),
 
     (* Duplicated key in context *)
-    (2 <# l-len buffer) *
-    (#rawKC == l-sub (buffer, 0, 2)) *
+    (2i <# (l-len buffer)) *
+    (#rawKC == l-sub (buffer, 0i, 2i)) *
     rawToUInt16(#rawKC, false, #keyCount) *
     (0 <# #keyCount) *
     Elements("Complete", buffer, 2, #keyCount, 2, ECKs, #ECKsLength) *
     toUtf8PairMap(ECKs, #utf8ECKs) * FirstProj(ECKs, #ECKeys) * Duplicated({{ }}, #ECKeys) *
-    (2 + #ECKsLength == l-len buffer) *
+    (as_int (2 + #ECKsLength) == l-len buffer) *
     (errorMessage == "decodeEncryptionContext: Duplicate encryption context key value.");
 
 (* General serialised encryption context *)
@@ -569,25 +586,26 @@ nounfold pred CHeader(+rawHeaderData, part_one, version, type, suiteId,
                       contentType, headerIvLength, frameLength, headerLength,
                       headerIv, headerAuthTag) :
   (rawHeaderData == l+ (part_one, part_two)) *
-    ((l-len part_one) == 22) *
+    ((l-len part_one) == 22i) *
     (part_one == l+ ({{ version, type }}, #rawSuiteId, messageId, #rawContextLength)) *
-    ((l-len #rawSuiteId) == 2) *
-    ((l-len messageId) == 16) *
-    ((l-len #rawContextLength) == 2) * CVersionAndType(version, type) *
+    ((l-len #rawSuiteId) == 2i) *
+    ((l-len messageId) == 16i) *
+    ((l-len #rawContextLength) == 2i) * CVersionAndType(version, type) *
     rawToUInt16(#rawSuiteId, false, suiteId) *
     CAlgorithmSuite(suiteId, #stringId, headerIvLength, #tagLength) *
     rawToUInt16(#rawContextLength, false, ECLength) *
     (part_two == l+ (#EC, part_three)) *
-    ((l-len #EC) == ECLength) *
+    ((l-len #EC) == as_int ECLength) *
     CRawEncryptionContext(#EC, ECKs) *
     (part_three == l+ (#edks, {{ contentType }}, {{ 0, 0, 0, 0 }}, {{ headerIvLength }}, #rawFrameLength, headerIv, headerAuthTag)) *
     RawEncryptedDataKeys("Complete", rawHeaderData, (22 + ECLength), EDKs, #EDKsLength, _) *
-    (#EDKsLength == (l-len #edks)) * ((l-len #rawFrameLength) == 4) *
+    (as_int #EDKsLength == (l-len #edks)) * ((l-len #rawFrameLength) == 4i) *
     rawToUInt32(#rawFrameLength, false, frameLength) *
     (headerLength == ((((((22 + ECLength) + #EDKsLength) + 1) + 4) + 1) + 4)) *
-    ((l-len headerIv) == headerIvLength) *
-    ((l-len headerAuthTag) == (#tagLength / 8)) *
-    (((headerLength + headerIvLength) + (#tagLength / 8)) <=# (l-len rawHeaderData));
+    ((l-len headerIv) == as_int headerIvLength) *
+    ((l-len headerAuthTag) == as_int (#tagLength / 8)) *
+    (((headerLength + headerIvLength) + (#tagLength / 8)) <=# as_num (l-len rawHeaderData));
+  facts: (is_int suiteId) and (is_int ECLength) and (is_int headerIvLength) and (is_int frameLength) and (is_int headerLength);
 
 (* Serialised incomplete header *)
 @nopath
@@ -675,7 +693,7 @@ nounfold pred BHeader(+rawHeaderData, part_one, version, type, suiteId, messageI
                                       part_two, ECKs,
                                       part_three, EDKs, contentType, headerIvLength, frameLength, headerLength, headerIv, headerAuthTag, errorMessage) :
     (* Incorrect version and/or type *)
-    (22 <=# l-len rawHeaderData) *
+    (22 <=# as_num (l-len rawHeaderData)) *
     (rawHeaderData == l+ ({{ version, type }}, #rest)) *
     BVersionAndType(version, type, errorMessage) *
 
@@ -686,9 +704,9 @@ nounfold pred BHeader(+rawHeaderData, part_one, version, type, suiteId, messageI
     (frameLength == 0) * (headerLength == 0) * (headerIv == {{ }}) * (headerAuthTag == {{ }}),
 
     (* Unsupported algorithm suite *)
-    (22 <=# l-len rawHeaderData) *
+    (22 <=# as_num (l-len rawHeaderData)) *
     (rawHeaderData == l+ ({{ version, type }}, #rawSuiteId, #rest)) *
-    (l-len #rawSuiteId == 2) *
+    (l-len #rawSuiteId == 2i) *
     CVersionAndType(version, type) *
     rawToUInt16(#rawSuiteId, false, suiteId) *
     BAlgorithmSuite(suiteId, errorMessage) *
@@ -699,42 +717,42 @@ nounfold pred BHeader(+rawHeaderData, part_one, version, type, suiteId, messageI
     (frameLength == 0) * (headerLength == 0) * (headerIv == {{ }}) * (headerAuthTag == {{ }}),
 
     (* Broken encryption context *)
-    (22 <=# l-len rawHeaderData) *
+    (22 <=# as_num (l-len rawHeaderData)) *
     (rawHeaderData == l+ (part_one, part_two)) *
-    (l-len part_one == 22) *
+    (l-len part_one == 22i) *
     (part_one == l+ ({{ version, type }}, #rawSuiteId, messageId, #rawContextLength)) *
-    (l-len #rawSuiteId == 2) *
-    (l-len messageId == 16) *
-    (l-len #rawContextLength == 2) *
+    (l-len #rawSuiteId == 2i) *
+    (l-len messageId == 16i) *
+    (l-len #rawContextLength == 2i) *
     CVersionAndType(version, type) *
     rawToUInt16(#rawSuiteId, false, suiteId) *
     CAlgorithmSuite(suiteId, #stringId, headerIvLength, #tagLength) *
     rawToUInt16(#rawContextLength, false, ECLength) *
-    (22 + ECLength <=# l-len rawHeaderData) *
+    (22 + ECLength <=# as_num (l-len rawHeaderData)) *
 
     (part_two == l+ (#EC, part_three)) *
-    (l-len #EC == ECLength) *
+    (l-len #EC == as_int ECLength) *
     BRawEncryptionContext(errorMessage, #EC, ECKs) *
 
     (EDKs == {{ }}) * (contentType == 0) * (frameLength == 0) *
     (headerLength == 0) * (headerIv == {{ }}) * (headerAuthTag == {{ }}),
 
     (* Broken encrypted data keys *)
-    (22 <=# l-len rawHeaderData) *
+    (22 <=# as_num (l-len rawHeaderData)) *
     (rawHeaderData == l+ (part_one, part_two)) *
-    (l-len part_one == 22) *
+    (l-len part_one == 22i) *
     (part_one == l+ ({{ version, type }}, #rawSuiteId, messageId, #rawContextLength)) *
-    (l-len #rawSuiteId == 2) *
-    (l-len messageId == 16) *
-    (l-len #rawContextLength == 2) *
+    (l-len #rawSuiteId == 2i) *
+    (l-len messageId == 16i) *
+    (l-len #rawContextLength == 2i) *
     CVersionAndType(version, type) *
     rawToUInt16(#rawSuiteId, false, suiteId) *
     CAlgorithmSuite(suiteId, #stringId, headerIvLength, #tagLength) *
     rawToUInt16(#rawContextLength, false, ECLength) *
-    (22 + ECLength <=# l-len rawHeaderData) *
+    (22 + ECLength <=# as_num (l-len rawHeaderData)) *
 
     (part_two == l+ (#EC, part_three)) *
-    (l-len #EC == ECLength) *
+    (l-len #EC == as_int ECLength) *
     CRawEncryptionContext(#EC, ECKs) *
     RawEncryptedDataKeys("Broken", rawHeaderData, 22 + ECLength, _, _, errorMessage) *
 
@@ -742,56 +760,56 @@ nounfold pred BHeader(+rawHeaderData, part_one, version, type, suiteId, messageI
     (headerLength == 0) * (headerIv == {{ }}) * (headerAuthTag == {{ }}),
 
     (* Incorrect reserved bytes *)
-    (22 <=# l-len rawHeaderData) *
+    (22 <=# as_num (l-len rawHeaderData)) *
     (rawHeaderData == l+ (part_one, part_two)) *
-    (l-len part_one == 22) *
+    (l-len part_one == 22i) *
     (part_one == l+ ({{ version, type }}, #rawSuiteId, messageId, #rawContextLength)) *
-    (l-len #rawSuiteId == 2) *
-    (l-len messageId == 16) *
-    (l-len #rawContextLength == 2) *
+    (l-len #rawSuiteId == 2i) *
+    (l-len messageId == 16i) *
+    (l-len #rawContextLength == 2i) *
     CVersionAndType(version, type) *
     rawToUInt16(#rawSuiteId, false, suiteId) *
     CAlgorithmSuite(suiteId, #stringId, headerIvLength, #tagLength) *
     rawToUInt16(#rawContextLength, false, ECLength) *
-    (22 + ECLength <=# l-len rawHeaderData) *
+    (22 + ECLength <=# as_num (l-len rawHeaderData)) *
 
     (part_two == l+ (#EC, part_three)) *
-    (l-len #EC == ECLength) *
+    (l-len #EC == as_int ECLength) *
     CRawEncryptionContext(#EC, ECKs) *
     (part_three == l+ (#edks, {{ contentType }}, #rawReservedBytes, #rest)) *
     RawEncryptedDataKeys("Complete", rawHeaderData, 22 + ECLength, EDKs, #EDKsLength, _) *
-    (#EDKsLength == l-len #edks) *
-    (l-len #rawReservedBytes == 4) *
+    (#EDKsLength == as_num (l-len #edks)) *
+    (l-len #rawReservedBytes == 4i) *
     rawToUInt32(#rawReservedBytes, false, #reservedBytes) *
     (! (#reservedBytes == 0)) *
     (headerLength == 22 + ECLength + #EDKsLength + 1 + 4 + 1 + 4) *
-    (headerLength + headerIvLength + (#tagLength / 8) <=# l-len rawHeaderData) *
+    (headerLength + headerIvLength + (#tagLength / 8) <=# as_num (l-len rawHeaderData)) *
 
     (errorMessage == "Malformed Header: Reserved bytes not equal to zero.") *
     (frameLength == 0) * (headerIv == {{ }}) * (headerAuthTag == {{ }}),
 
     (* IV length mismatch *)
-    (22 <=# l-len rawHeaderData) *
+    (22 <=# as_num (l-len rawHeaderData)) *
     (rawHeaderData == l+ (part_one, part_two)) *
-    (l-len part_one == 22) *
+    (l-len part_one == 22i) *
     (part_one == l+ ({{ version, type }}, #rawSuiteId, messageId, #rawContextLength)) *
-    (l-len #rawSuiteId == 2) *
-    (l-len messageId == 16) *
-    (l-len #rawContextLength == 2) *
+    (l-len #rawSuiteId == 2i) *
+    (l-len messageId == 16i) *
+    (l-len #rawContextLength == 2i) *
     CVersionAndType(version, type) *
     rawToUInt16(#rawSuiteId, false, suiteId) *
     CAlgorithmSuite(suiteId, #stringId, #ivLength, #tagLength) *
     rawToUInt16(#rawContextLength, false, ECLength) *
-    (22 + ECLength <=# l-len rawHeaderData) *
+    (22 + ECLength <=# as_num (l-len rawHeaderData)) *
 
     (part_two == l+ (#EC, part_three)) *
-    (l-len #EC == ECLength) *
+    (l-len #EC == as_int ECLength) *
     CRawEncryptionContext(#EC, ECKs) *
     (part_three == l+ (#edks, {{ contentType }}, {{ 0, 0, 0, 0 }}, {{ headerIvLength }}, #rest)) *
     RawEncryptedDataKeys("Complete", rawHeaderData, 22 + ECLength, EDKs, #EDKsLength, _) *
-    (#EDKsLength == l-len #edks) *
+    (#EDKsLength == as_num (l-len #edks)) *
     (headerLength == 22 + ECLength + #EDKsLength + 1 + 4 + 1 + 4) *
-    (headerLength + #ivLength + (#tagLength / 8) <=# l-len rawHeaderData) *
+    (headerLength + #ivLength + (#tagLength / 8) <=# as_num (l-len rawHeaderData)) *
     (! (headerIvLength == #ivLength)) *
 
     (errorMessage == "Malformed Header: Mismatch between expected and obtained IV length.") *
diff --git a/Gillian-JS/Examples/Amazon/ListLogic.gil b/Gillian-JS/Examples/Amazon/ListLogic.gil
index 62bd23e8..016859f4 100644
--- a/Gillian-JS/Examples/Amazon/ListLogic.gil
+++ b/Gillian-JS/Examples/Amazon/ListLogic.gil
@@ -179,7 +179,7 @@ lemma ListToSetAddElement(lst, set, element)
     ListToSet(l+ (#lst, {{ #element }}), -u- (#set, -{ #element }-))
 ]]
 [*
-    unfold ListToSet(#lst, #element);
+    unfold ListToSet(#lst, #set);
     if (!(#lst == {{ }})) then {
         sep_assert ((#lst == l+ ({{ #fProp }}, #restLst))) [bind: #fProp, #restLst];
         sep_assert (ListToSet(#restLst, #restSet)) [bind: #restSet];
diff --git a/Gillian-JS/Examples/Amazon/deserialize_factory.js b/Gillian-JS/Examples/Amazon/deserialize_factory.js
index 15c074b6..83add78c 100644
--- a/Gillian-JS/Examples/Amazon/deserialize_factory.js
+++ b/Gillian-JS/Examples/Amazon/deserialize_factory.js
@@ -128,7 +128,6 @@ function readElements(elementCount, fieldsPerElement, buffer, readPos) {
         [bind: #doneEl, #innerLoopReadPos, #fLeft, #remElList, #remElLength, #doneElList, #doneElLength] */
     while (fieldCount--) {
       /* @tactic
-          unfold innerLoopInvariantFacts(#definition, #remElsList, #view, #innerLoopReadPos, #fLeft, #remElList, #eLength, #remElsLength, #doneElLength, #remElLength);
           if (#definition = "Complete") then {
               unfold CElement(#view, #innerLoopReadPos, #fLeft, #remElList, #remElLength)
           } else {
@@ -809,19 +808,7 @@ function deserializeMessageHeader(messageBuffer) {
 
   var suiteId = dataView.getUint16(2, false)  // big endian
   /* Precondition: suiteId must match supported algorithm suite */
-  /*
-    @tactic
-        if (#definition = "Complete") then {
-            unfold CAlgorithmSuite(#suiteId, #stringId, #headerIvLength, #tagLength)
-        }
-  */
   needs(AlgorithmSuiteIdentifier[suiteId], 'Malformed Header: Unsupported algorithm suite.')
-  /*
-    @tactic
-        if (#definition = "Complete") then {
-            fold CAlgorithmSuite(#suiteId, #stringId, #headerIvLength, #tagLength)
-        }
-  */
   var messageId = messageBuffer.slice(4, 20)
   var contextLength = dataView.getUint16(20, false) // big endian
 
diff --git a/Gillian-JS/runtime/JSLogic/ArrayBuffer.jsil b/Gillian-JS/runtime/JSLogic/ArrayBuffer.jsil
index 5a67dfad..9a7afd6f 100644
--- a/Gillian-JS/runtime/JSLogic/ArrayBuffer.jsil
+++ b/Gillian-JS/runtime/JSLogic/ArrayBuffer.jsil
@@ -15,7 +15,7 @@ nounfold pred ArrayBuffer (+ab:Obj, data:List) :
   ((#md, "@extensible")            -> true) *          (* Array buffers are extensible                   *)
   ((#md, "@ArrayBufferData")       -> data) *          (* Array buffer contents                          *)
   ((#md, "@ArrayBufferByteLength") -> #len_data) *     (* Array buffer length                            *)
-  (#len_data == l-len data) *
+  ((as_int #len_data) == l-len data) *
 
   (* No other internal properties *)
   empty_fields (#md : -{ "@class", "@extensible", "@proto", "@ArrayBufferData", "@ArrayBufferByteLength" }-);
@@ -44,7 +44,7 @@ nounfold pred ArrayBufferPrototype (proto) :
 
 axiomatic spec ABP_byteLength (xsc, vthis)
     [[ (vthis == #vthis) * ArrayBuffer(#vthis, #data) ]]
-    [[ ArrayBuffer(#vthis, #data) * (ret == l-len #data) ]]
+    [[ ArrayBuffer(#vthis, #data) * (ret == (l-len #data)) ]]
     normal
 
 axiomatic spec ABP_slice (xsc, vthis, start, end)
diff --git a/Gillian-JS/runtime/JSLogic/ByteLogic.gil b/Gillian-JS/runtime/JSLogic/ByteLogic.gil
index 0dd63a9a..a86e9b60 100644
--- a/Gillian-JS/runtime/JSLogic/ByteLogic.gil
+++ b/Gillian-JS/runtime/JSLogic/ByteLogic.gil
@@ -7,47 +7,53 @@
  ****************************************)
 
 (* Interpretation: one byte as an unsigned 8-bit integer *)
-pure pred rawToUInt8(+bytes:List, x:Int) :
+pure pred rawToUInt8(+bytes:List, x:Num) :
     (bytes == {{ #b0 }}) * (x == #b0) *
-    (0i i<=# #b0) * (#b0 i<# 256i);
-
-pure pred rawToUInt8JS(+bytes:List, n:Num) :
-    rawToUInt8(bytes, #x) * (n == (as_num #x));
+    (0 <=# #b0) * (#b0 <# 256.) *
+    (is_int #b0);
 
 (* Interpretation: two bytes as an unsigned 16-bit integer *)
 @nopath
-pure pred rawToUInt16(+bytes:List, +littleEndian:Bool, x:Int) :
+pure pred rawToUInt16(+bytes:List, +littleEndian:Bool, x:Num) :
     (littleEndian == false) *
       (bytes == {{ #b0, #b1 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (x == (#b0 i* 256i) i+ #b1),
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (x == (#b0 * 256.) + #b1) *
+      (is_int #b0) *
+      (is_int #b1),
     (littleEndian == true) *
       (bytes == {{ #b0, #b1 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (x == (#b1 i* 256i) i+ #b0);
-
-pure pred rawToUInt16JS(+bytes:List, +littleEndian:Bool, n:Num) :
-    rawToUInt16(bytes, littleEndian, #x) * (n == (as_num #x));
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (x == (#b1 * 256.) + #b0) *
+      (is_int #b0) *
+      (is_int #b1);
+  facts: (is_int x);
 
 (* Interpretation: four bytes as an unsigned 32-bit integer *)
 @nopath
-pure pred rawToUInt32(+bytes:List, +littleEndian:Bool, x:Int) :
+pure pred rawToUInt32(+bytes:List, +littleEndian:Bool, x:Num) :
     (littleEndian == false) *
       (bytes == {{ #b0, #b1, #b2, #b3 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (0i i<=# #b2) * (#b2 i<# 256i) *
-      (0i i<=# #b3) * (#b3 i<# 256i) *
-      (x == (#b0 i* 16777216i) i+ (#b1 i* 65536i) i+ (#b2 i* 256i) i+ #b3),
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (0. <=# #b2) * (#b2 <# 256.) *
+      (0. <=# #b3) * (#b3 <# 256.) *
+      (x == (#b0 * 16777216.) + (#b1 * 65536.) + (#b2 * 256.) + #b3) *
+      (is_int #b0) *
+      (is_int #b1) *
+      (is_int #b2) *
+      (is_int #b3),
     (littleEndian == true) *
       (bytes == {{ #b0, #b1, #b2, #b3 }}) *
-      (0i i<=# #b0) * (#b0 i<# 256i) *
-      (0i i<=# #b1) * (#b1 i<# 256i) *
-      (0i i<=# #b2) * (#b2 i<# 256i) *
-      (0i i<=# #b3) * (#b3 i<# 256i) *
-      (x == (#b3 i* 16777216i) i+ (#b2 i* 65536i) i+ (#b1 i* 256i) i+ #b0);
-
-pure pred rawToUInt32JS(+bytes:List, +littleEndian:Bool, n:Num) :
-    rawToUInt32(bytes, littleEndian, #x) * (n == (as_num #x));
+      (0. <=# #b0) * (#b0 <# 256.) *
+      (0. <=# #b1) * (#b1 <# 256.) *
+      (0. <=# #b2) * (#b2 <# 256.) *
+      (0. <=# #b3) * (#b3 <# 256.) *
+      (x == (#b3 * 16777216.) + (#b2 * 65536.) + (#b1 * 256.) + #b0) *
+      (is_int #b0) *
+      (is_int #b1) *
+      (is_int #b2) *
+      (is_int #b3);
+    facts: (is_int x);
diff --git a/Gillian-JS/runtime/JSLogic/DataView.jsil b/Gillian-JS/runtime/JSLogic/DataView.jsil
index 827549bc..5472fac0 100644
--- a/Gillian-JS/runtime/JSLogic/DataView.jsil
+++ b/Gillian-JS/runtime/JSLogic/DataView.jsil
@@ -116,47 +116,47 @@ axiomatic spec DVP_byteOffset (xsc, vthis)
 axiomatic spec DVP_getUint8 (xsc, vthis, byteOffset)
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 1) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 1.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt8JS(#raw, ret) ]]
+       rawToUInt8(#raw, ret) ]]
     normal
 
 axiomatic spec DVP_getUint16 (xsc, vthis, byteOffset, littleEndian)
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == undefined) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 2) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 2.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt16JS(#raw, false, ret) ]]
+       rawToUInt16(#raw, false, ret) ]]
     normal;
 
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == #littleEndian) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 2) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 2.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (#raw== l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt16JS(#raw, #littleEndian, ret) ]]
+       (#raw == l-sub (#view, #byteOffset, #elementSize)) *
+       rawToUInt16(#raw, #littleEndian, ret) ]]
     normal
 
 axiomatic spec DVP_getUint32 (xsc, vthis, byteOffset, littleEndian)
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == undefined) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 4) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 4.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt32JS(#raw, false, ret) ]]
+       rawToUInt32(#raw, false, ret) ]]
     normal;
 
     [[ (vthis == #vthis) * (byteOffset == #byteOffset) * (littleEndian == #littleEndian) *
        DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
-       (0 <=# byteOffset) * (#elementSize == 4) * (#byteOffset + #elementSize <=# #viewSize) *
+       (0 <=# byteOffset) * (#elementSize == 4.) * (#byteOffset + #elementSize <=# #viewSize) *
        (#view == l-sub(#data, #viewOffset, #viewSize)) ]]
     [[ DataView(#vthis, #buffer, #viewOffset, #viewSize) * ArrayBuffer(#buffer, #data) *
        (#raw == l-sub (#view, #byteOffset, #elementSize)) *
-       rawToUInt32JS(#raw, #littleEndian, ret) ]]
+       rawToUInt32(#raw, #littleEndian, ret) ]]
     normal
\ No newline at end of file
diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml
index 22dce031..6381dbf4 100644
--- a/GillianCore/engine/Abstraction/PState.ml
+++ b/GillianCore/engine/Abstraction/PState.ml
@@ -587,22 +587,24 @@ module Make (State : SState.S) :
     (* This will not do anything in the original pass,
        but will do precisely what is needed in the re-establishment *)
     let vars_to_forget = SS.inter state_lvars (SS.of_list lvar_binders) in
-    if vars_to_forget <> SS.empty then (
-      let oblivion_subst = fresh_subst vars_to_forget in
-      L.verbose (fun m ->
-          m "Forget @[%a@] with subst: %a"
-            Fmt.(iter ~sep:comma SS.iter string)
-            vars_to_forget SVal.SESubst.pp oblivion_subst);
-
-      (* TODO: THIS SUBST IN PLACE MUST NOT BRANCH *)
-      let subst_in_place =
-        substitution_in_place ~subst_all:true oblivion_subst astate
-      in
-      assert (List.length subst_in_place = 1);
-      let astate = List.hd subst_in_place in
+    let astate =
+      if vars_to_forget <> SS.empty then (
+        let oblivion_subst = fresh_subst vars_to_forget in
+        L.verbose (fun m ->
+            m "Forget @[%a@] with subst: %a"
+              Fmt.(iter ~sep:comma SS.iter string)
+              vars_to_forget SVal.SESubst.pp oblivion_subst);
+
+        (* TODO: THIS SUBST IN PLACE MUST NOT BRANCH *)
+        let subst_in_place =
+          substitution_in_place ~subst_all:true oblivion_subst astate
+        in
+        assert (List.length subst_in_place = 1);
+        let astate = List.hd subst_in_place in
 
-      L.verbose (fun m -> m "State after substitution:@\n@[%a@]\n" pp astate))
-    else ();
+        L.verbose (fun m -> m "State after substitution:@\n@[%a@]\n" pp astate);
+        astate)
+      else astate in
     let mp =
       match mp with
       | Error asrts ->
@@ -628,6 +630,7 @@ module Make (State : SState.S) :
     let open Res_list.Syntax in
     let open Syntaxes.List in
     let** new_state, subst', _ =
+      L.verbose (fun m -> m "State before matching:@\n@[%a@]\n" pp astate);
       let+ result = SMatcher.match_ astate subst mp Invariant in
       match result with
       | Ok state -> Ok state
diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml
index aa403e46..0cf635e2 100644
--- a/GillianCore/engine/Abstraction/Verifier.ml
+++ b/GillianCore/engine/Abstraction/Verifier.ml
@@ -623,7 +623,7 @@ struct
     match test.flag with
     | Some _ ->
         let msg = "Verifying one spec of procedure " ^ test.name ^ "... " in
-        L.tmi (fun fmt -> fmt "%s" msg);
+        L.normal (fun fmt -> fmt "%s" msg);
         Fmt.pr "%s@?" msg;
         (* Reset coverage for every procedure in verification *)
         { prog with coverage = Hashtbl.create 1 }
@@ -656,7 +656,7 @@ struct
             else Ok () (* It's already correct *)
         | Some proof -> (
             let msg = "Verifying lemma " ^ test.name ^ "... " in
-            L.tmi (fun fmt -> fmt "%s" msg);
+            L.normal (fun fmt -> fmt "%s" msg);
             Fmt.pr "%s@?" msg;
             let lemma_evaluation_results =
               SAInterpreter.evaluate_lcmds prog proof state
diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index c9d18d9a..c27b6417 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -829,28 +829,56 @@ let rec reduce_binop_inttonum_const
   let open Utils.Syntaxes.Option in
   let f = reduce_lexpr_loop ~matching ~reduce_lvars pfs gamma in
   match (l, r) with
-  | Lit (Num x), UnOp (IntToNum, e) | UnOp (IntToNum, e), Lit (Num x) ->
-      let* () = if snd (modf x) = 0.0 then Some () else None in
-      let l = Expr.Lit (Int (Z.of_float x)) in
-      let r = f e in
-      let+ op =
-        BinOp.(
-          match op with
-          | Equal -> Some Equal
-          | FLessThan -> Some ILessThan
-          | FLessThanEqual -> Some ILessThanEqual
-          | FPlus -> Some IPlus
-          | FMinus -> Some IMinus
-          | FTimes -> Some ITimes
-          | BitwiseAndF -> Some BitwiseAnd
-          | BitwiseOrF -> Some BitwiseOr
-          | BitwiseXorF -> Some BitwiseXor
-          | LeftShiftF -> Some LeftShiftF
-          | SignedRightShiftF -> Some SignedRightShift
-          | UnsignedRightShiftF -> Some UnsignedRightShift
-          | _ -> None)
-      in
-      Expr.BinOp (l, op, r)
+  | Lit (Num x), UnOp (IntToNum, e) ->
+    let* () = if snd (modf x) = 0.0 then Some () else None in
+    let l = Expr.Lit (Int (Z.of_float x)) in
+    let r = f e in
+    let+ (wrap, op) =
+      BinOp.(
+        match op with
+        | Equal -> Some (false, Equal)
+        | FLessThan -> Some (false, ILessThan)
+        | FLessThanEqual -> Some (false, ILessThanEqual)
+        | FPlus -> Some (true, IPlus)
+        | FMinus -> Some (true, IMinus)
+        | FTimes -> Some (true, ITimes)
+        | BitwiseAndF -> Some (true, BitwiseAnd)
+        | BitwiseOrF -> Some (true, BitwiseOr)
+        | BitwiseXorF -> Some (true, BitwiseXor)
+        | LeftShiftF -> Some (true, LeftShiftF)
+        | SignedRightShiftF -> Some (true, SignedRightShift)
+        | UnsignedRightShiftF -> Some (true, UnsignedRightShift)
+        | _ -> None)
+    in
+    let res = Expr.BinOp (l, op, r) in
+    (match wrap with
+    | true -> Expr.UnOp (IntToNum, res)
+    | false -> res)
+  | UnOp (IntToNum, e), Lit (Num x) ->
+    let* () = if snd (modf x) = 0.0 then Some () else None in
+    let r = Expr.Lit (Int (Z.of_float x)) in
+    let l = f e in
+    let+ (wrap, op) =
+      BinOp.(
+        match op with
+        | Equal -> Some (false, Equal)
+        | FLessThan -> Some (false, ILessThan)
+        | FLessThanEqual -> Some (false, ILessThanEqual)
+        | FPlus -> Some (true, IPlus)
+        | FMinus -> Some (true, IMinus)
+        | FTimes -> Some (true, ITimes)
+        | BitwiseAndF -> Some (true, BitwiseAnd)
+        | BitwiseOrF -> Some (true, BitwiseOr)
+        | BitwiseXorF -> Some (true, BitwiseXor)
+        | LeftShiftF -> Some (true, LeftShiftF)
+        | SignedRightShiftF -> Some (true, SignedRightShift)
+        | UnsignedRightShiftF -> Some (true, UnsignedRightShift)
+        | _ -> None)
+    in
+    let res = Expr.BinOp (l, op, r) in
+    (match wrap with
+    | true -> Expr.UnOp (IntToNum, res)
+    | false -> res)
   | _ -> None
 
 (** Reduction of logical expressions
@@ -1054,6 +1082,18 @@ and reduce_lexpr_loop
     | LstSub (e1, Lit (Int z), e3)
       when Z.equal z Z.zero
            && List.mem (Cint.of_expr e3) (find_list_length_eqs pfs e1) -> e1
+    | LstSub (e1, e2, e3)
+      when
+        SS.inter (Expr.lvars e1) (Expr.lvars e3) = SS.empty
+          &&
+        List.length (
+          List.filter (fun e -> SS.inter (Expr.lvars e) (Expr.lvars e3) != SS.empty) (get_equal_expressions pfs e1)
+        ) > 0
+      ->
+        let eqs = get_equal_expressions pfs e1 in
+        let e1' = List.hd (List.filter (fun e -> SS.inter (Expr.lvars e) (Expr.lvars e3) != SS.empty) eqs) in
+        L.verbose (fun fmt -> fmt "Replacement LstSub: %a -> %a" Expr.pp e1 Expr.pp e1');
+        LstSub (e1', e2, e3)
     | LstSub (le1, le2, le3) -> (
         let fle1 = f le1 in
         let fle2 = substitute_for_list_length pfs (f le2) in
@@ -1330,6 +1370,44 @@ and reduce_lexpr_loop
     | UnOp (LstLen, LstSub (_, _, e)) -> e
     | UnOp (IntToNum, UnOp (NumToInt, le)) when PFS.mem pfs (UnOp (IsInt, le))
       -> le
+    (* Conversions *)
+    | UnOp (IntToNum, BinOp (le1, IPlus, le2)) ->
+        BinOp ((UnOp (IntToNum, le1)), FPlus, (UnOp (IntToNum, le2)))
+    | UnOp (NumToInt, BinOp (le1, FPlus, le2)) ->
+        BinOp ((UnOp (NumToInt, le1)), IPlus, (UnOp (NumToInt, le2)))
+    | UnOp (NumToInt, BinOp (le1, FTimes, le2)) ->
+        BinOp ((UnOp (NumToInt, le1)), ITimes, (UnOp (NumToInt, le2)))
+    | UnOp (IntToNum, UnOp (LstLen, x))
+      when
+        List.length
+          (get_equal_expressions pfs (UnOp (LstLen, x))
+          |> List.filter (fun x -> match x with | Expr.UnOp (NumToInt, _) -> true | _ -> false)) = 1
+      ->
+        L.verbose (fun fmt -> fmt "l-len conversion: %a" Expr.pp le);
+        let eqs =
+          (get_equal_expressions pfs (UnOp (LstLen, x))
+          |> List.filter (fun x -> match x with | Expr.UnOp (NumToInt, _) -> true | _ -> false)) in
+        (match List.hd eqs with
+        | UnOp (NumToInt, e) -> e
+        | _ -> raise (ReductionException (le, "Impossible")))
+    (* IsInt *)
+    | UnOp (IsInt, UnOp (IntToNum, _)) -> Lit (Bool true)
+    | UnOp (IsInt, Lit (Num n)) -> Lit (Bool (Float.is_integer n))
+    | UnOp (IsInt, BinOp (le', FPlus, re'))
+    | UnOp (IsInt, BinOp (le', FMinus, re'))
+    | UnOp (IsInt, BinOp (le', FTimes, re')) ->
+        let resl = f (UnOp (IsInt, le')) in
+        L.verbose (fun fmt -> fmt "is_int_reduction: %a\n\tlhs: %a" Expr.pp le Expr.pp resl);
+        if resl = Lit (Bool true) || PFS.mem pfs resl then
+          UnOp (IsInt, re')
+        else (
+          let resr = f (UnOp (IsInt, re')) in
+           L.verbose (fun fmt -> fmt "\trhs: %a" Expr.pp resr);
+          if (f (UnOp (IsInt, re')) = Lit (Bool true)) || PFS.mem pfs resr then
+            UnOp (IsInt, le')
+          else
+            le
+        )
     (* Number-to-string-to-number-to-string-to... *)
     | UnOp (ToNumberOp, UnOp (ToStringOp, le)) -> (
         let fle = f le in
@@ -1709,8 +1787,14 @@ and reduce_lexpr_loop
       when Expr.equal a c || Expr.equal b c -> Expr.num 0.
     | BinOp (x, FTimes, BinOp (y, FDiv, z)) when x = z -> y
     | BinOp (BinOp (x, FDiv, y), FTimes, z) when y = z -> x
-    | BinOp (UnOp (NumToInt, x), Equal, y) | BinOp (y, Equal, UnOp (NumToInt, x))
-      -> BinOp (UnOp (IntToNum, y), Equal, x)
+    | BinOp (UnOp (NumToInt, x), Equal, y)
+        when (match y with
+        | UnOp (LstLen, _) -> false
+        | _ -> true) -> BinOp (UnOp (IntToNum, y), Equal, x)
+    | BinOp (y, Equal, UnOp (NumToInt, x))
+        when (match y with
+        | UnOp (LstLen, _) -> false
+        | _ -> true) -> BinOp (UnOp (IntToNum, y), Equal, x)
     (* BinOps: Equalities (strings) *)
     (* x = y ++ z
           /\ |x| < |y| => false
@@ -2239,16 +2323,19 @@ and simplify_num_arithmetic_lexpr
   | BinOp (l, FPlus, Lit (Num 0.)) | BinOp (Lit (Num 0.), FPlus, l) -> l
   (* Binary minus to unary minus *)
   | BinOp (l, FMinus, r) -> f (BinOp (l, FPlus, UnOp (FUnaryMinus, r)))
-  (* Unary minus distributes over + *)
+  (* Unary minus distributes over +, - *)
   | UnOp (FUnaryMinus, e) -> (
       match e with
       | BinOp (l, FPlus, r) ->
           f (BinOp (UnOp (FUnaryMinus, l), FPlus, UnOp (FUnaryMinus, r)))
+      | BinOp (l, FMinus, r) ->
+          f (BinOp (UnOp (FUnaryMinus, l), FPlus, r))
       | _ -> le)
   (* FPlus - we collect the positives and the negatives, see what we have and deal with them *)
   | BinOp (l, FPlus, r) ->
       let cl = Cnum.of_expr l in
       let cr = Cnum.of_expr r in
+      L.verbose (fun fmt -> fmt "FPlus check:\n\t%a\t-->\t%a\n\t%a\t-->\t%a" Expr.pp l Expr.pp (Cnum.to_expr cl) Expr.pp r Expr.pp (Cnum.to_expr cr));
       Cnum.to_expr (Cnum.plus cl cr)
   | _ -> le
 
diff --git a/GillianCore/engine/FOLogic/Simplifications.ml b/GillianCore/engine/FOLogic/Simplifications.ml
index c75fbff4..ef8df2f0 100644
--- a/GillianCore/engine/FOLogic/Simplifications.ml
+++ b/GillianCore/engine/FOLogic/Simplifications.ml
@@ -681,6 +681,20 @@ let simplify_pfs_and_gamma
                     | Some tv ->
                         if t <> tv then stop_explain "Type mismatch"
                         else `Filter)
+                (* Int breakdown *)
+                | Lit (Num n), BinOp (l, FPlus, BinOp (Lit (Num 256.), FTimes, r))
+                  when
+                    PFS.mem pfs (BinOp (Lit (Num 0.), FLessThanEqual, l)) &&
+                    PFS.mem pfs (BinOp (Lit (Num 0.), FLessThanEqual, r)) &&
+                    PFS.mem pfs (BinOp (l, FLessThan, Lit (Num 256.))) &&
+                    PFS.mem pfs (BinOp (r, FLessThan, Lit (Num 256.)))
+                    ->
+                  let n = int_of_float n in
+                  let eq_l = Expr.BinOp (l, Equal, Lit (Num (float_of_int (n mod 256)))) in
+                  let eq_r = Expr.BinOp (r, Equal, Lit (Num (float_of_int (n / 256)))) in
+                  L.verbose (fun fmt -> fmt "Breakdown:\n\tn : %d\n\tl : %a\n\tr : %a" n Expr.pp eq_l Expr.pp eq_r);
+                  extend_with eq_l;
+                  `Replace eq_r
                 | _, _ -> `Replace whole))
         (* All other cases *)
         | _ -> `Replace whole
@@ -893,7 +907,7 @@ let simplify_pfs_and_gamma
                     (BinOp
                        ( Expr.zero_i,
                          ILessThanEqual,
-                         UnOp (LstLen, Expr.from_var_name v) ))
+                         UnOp (LstLen, Expr.from_var_name v) ));
               | _ -> ());
 
           analyse_list_structure lpfs;
diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
index f9bd1fc5..855a027d 100644
--- a/GillianCore/engine/general_semantics/general/g_interpreter.ml
+++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -846,23 +846,6 @@ struct
           in
           L.verbose (fun fmt ->
               fmt "Run_spec returned %d Results" (List.length ret));
-          if ret = [] then
-            if spec.data.spec_incomplete then (
-              L.normal (fun fmt -> fmt "Proceeding with symbolic execution.");
-              symb_exec_proc ())
-            else
-              [
-                eval_state_to_err ~error_state:state
-                  ~errors:
-                    [
-                      EState
-                        (EOther
-                           (Fmt.str "Unable to use specification of function %s"
-                              spec.data.spec_name));
-                    ]
-                  eval_state;
-              ]
-          else
             let successes, errors =
               List.partition_map
                 (function
@@ -870,20 +853,24 @@ struct
                   | Error x -> Right (Exec_err.EState x))
                 ret
             in
-            let spec_name = spec.data.spec_name in
-            let success_confs =
-              successes
-              |> List.mapi (fun ix (ret_state, fl) ->
-                     process_ret pid j eval_state ix ret_state fl
-                       (eval_state.b_counter + 1) true spec_name)
-            in
-            let error_confs =
-              match errors with
-              | [] -> []
-              | errors ->
-                  [ eval_state_to_err ~error_state:state ~errors eval_state ]
-            in
-            success_confs @ error_confs
+            if errors != [] && spec.data.spec_incomplete then (
+              L.normal (fun fmt -> fmt "Proceeding with symbolic execution.");
+              symb_exec_proc ()
+            ) else (
+              let spec_name = spec.data.spec_name in
+              let success_confs =
+                successes
+                |> List.mapi (fun ix (ret_state, fl) ->
+                      process_ret pid j eval_state ix ret_state fl
+                        (eval_state.b_counter + 1) true spec_name)
+              in
+              let error_confs =
+                match errors with
+                | [] -> []
+                | errors ->
+                    [ eval_state_to_err ~error_state:state ~errors eval_state ]
+              in
+              success_confs @ error_confs)
 
         let f x pid v_args j subst eval_state =
           let { prog; cs; state; _ } = eval_state in
diff --git a/GillianCore/gil_parser/GIL_Lexer.mll b/GillianCore/gil_parser/GIL_Lexer.mll
index af3046c3..1196f2ec 100644
--- a/GillianCore/gil_parser/GIL_Lexer.mll
+++ b/GillianCore/gil_parser/GIL_Lexer.mll
@@ -57,6 +57,7 @@
         "m_sin",         GIL_Parser.M_SIN;
         "m_sqrt",        GIL_Parser.M_SQRT;
         "m_tan",         GIL_Parser.M_TAN;
+        "is_int",        GIL_Parser.ISINT;
         "as_int",        GIL_Parser.NUMTOINT;
         "as_num",        GIL_Parser.INTTONUM;
         "num_to_string", GIL_Parser.TOSTRING;
diff --git a/GillianCore/smt/smt.ml b/GillianCore/smt/smt.ml
index 9a3e5962..8302c694 100644
--- a/GillianCore/smt/smt.ml
+++ b/GillianCore/smt/smt.ml
@@ -684,7 +684,7 @@ let encode_unop ~llen_lvars ~e (op : UnOp.t) le =
   | LstRev -> Axiomatised_operations.lrev <| get_list le >- ListType
   | NumToInt -> get_num le |> real_to_int >- IntType
   | IntToNum -> get_int le |> int_to_real >- NumberType
-  | IsInt -> num_divisible (get_num le) 1 >- BooleanType
+  | IsInt -> encode_equality (get_num le |> real_to_int |> int_to_real >- NumberType) le
   | BitwiseNot
   | M_isNaN
   | M_abs
diff --git a/transformers/lib/prebuilt/C.ml b/transformers/lib/prebuilt/C.ml
index dd84b9d6..ff7790b0 100644
--- a/transformers/lib/prebuilt/C.ml
+++ b/transformers/lib/prebuilt/C.ml
@@ -98,8 +98,8 @@ module ExtendMemory (S : C_PMapType) = struct
           BlockTree.get_fixes e |> map_fixes BlockTree.pred_to_str
       | _ -> []
 
-    let get_recovery_tactic = function
-      | BaseError e -> S.get_recovery_tactic e
+    let get_recovery_tactic s = function
+      | BaseError e -> S.get_recovery_tactic s e
       | BlockTreeErr (dest_idx, src_idx, _) ->
           Gillian.General.Recovery_tactic.try_unfold [ dest_idx; src_idx ]
       | _ -> Gillian.General.Recovery_tactic.none
diff --git a/transformers/lib/prebuilt/JSIL.ml b/transformers/lib/prebuilt/JSIL.ml
index be81b71c..9be40fde 100644
--- a/transformers/lib/prebuilt/JSIL.ml
+++ b/transformers/lib/prebuilt/JSIL.ml
@@ -46,7 +46,7 @@ module DeleteActionAddition (S : MyMonadicSMemory) :
   let execute_action Delete _ _ = Delayed.return (Ok (S.empty (), []))
   let can_fix () = false
   let get_fixes () = []
-  let get_recovery_tactic () = Gillian.General.Recovery_tactic.none
+  let get_recovery_tactic _ () = Gillian.General.Recovery_tactic.none
 end
 
 (* the "Props" predicate considers its out an in, so it must be removed
@@ -119,6 +119,7 @@ end
 module PatchDomainsetObject (S : sig
   include MyMonadicSMemory
 
+  val get_nonos : t -> Expr.t list
   val is_not_nono : t -> Expr.t -> bool
 end) =
   Injector
@@ -127,15 +128,21 @@ end) =
 
       let post_execute_action a (s, args, rets) =
         match (a, rets) with
-        | "get_domainset", [ (Expr.Lit (LList _) as dom) ]
-        | "get_domainset", [ (Expr.EList _ as dom) ] ->
-            let dom =
-              (match dom with
-              | Expr.Lit (LList lits) -> List.map Expr.lit lits
-              | Expr.EList lits -> lits
-              | _ -> failwith "Unexpected domainset type")
-              |> List.filter (S.is_not_nono s)
-              |> Expr.list
+        | "get_domainset", [ dom ] ->
+            let open Delayed.Syntax in
+            let* dom =
+              match dom with
+              | Expr.Lit (LList lits) ->
+                  List.map Expr.lit lits
+                  |> List.filter (S.is_not_nono s)
+                  |> Expr.list |> Delayed.return
+              | Expr.EList lits ->
+                  lits
+                  |> List.filter (S.is_not_nono s)
+                  |> Expr.list |> Delayed.return
+              | dom ->
+                  let nonos = Expr.ESet (S.get_nonos s) in
+                  Delayed.reduce (BinOp (dom, SetDiff, nonos))
             in
             Delayed.return (s, args, [ dom ])
         | _ -> Delayed.return (s, args, rets)
@@ -155,6 +162,8 @@ module BaseMemoryContent (S : MyMonadicSMemory) = struct
     PatchedProduct (IDs) (Mapper (JSSubstInner) (MoveInToOut (S))) (Agreement)
 
   include ActionAdder (DeleteActionAddition (S)) (S)
+
+  let get_metadata (_, s2) = s2
 end
 
 (* Override pretty printing, implement `is_not_nono` *)
@@ -174,6 +183,14 @@ module ObjectBase = struct
     in
     pf ft "[ @[%a@] | @[%a@] ]" pp_bindings h (option Expr.pp) d
 
+  let get_nonos (h, _) =
+    ExpMap.fold
+      (fun _ v acc ->
+        match v with
+        | Some (Expr.Lit Nono) -> Expr.Lit Nono :: acc
+        | _ -> acc)
+      h []
+
   let is_not_nono (h, _) idx =
     match ExpMap.find_opt idx h with
     | Some (Some (Expr.Lit Nono)) -> false
@@ -198,6 +215,17 @@ module SplitObjectBase = struct
     in
     pf ft "[ @[%a@] | @[%a@] ]" pp_bindings h (option Expr.pp) d
 
+  let get_nonos (((ch, sh), _) : t) =
+    let nonos_from_map m =
+      ExpMap.fold
+        (fun _ v acc ->
+          match v with
+          | Some (Expr.Lit Nono) -> Expr.Lit Nono :: acc
+          | _ -> acc)
+        m []
+    in
+    nonos_from_map ch @ nonos_from_map sh
+
   let is_not_nono ((ch, sh), _) idx =
     match ExpMap.find_opt idx ch with
     | Some (Some (Expr.Lit Nono)) -> false
@@ -224,7 +252,12 @@ module PatchedBasePMap (S : MyMonadicSMemory) :
 end
 
 (* Patch map pretty-printing for nicer diffs *)
-module PatchedALocPMap (S : MyMonadicSMemory) = struct
+module PatchedALocPMap (S : sig
+  include MyMonadicSMemory
+
+  val get_metadata : t -> Expr.t option
+end) =
+struct
   include OpenALocPMap (S)
 
   let pp ft (h : t) =
@@ -235,6 +268,39 @@ module PatchedALocPMap (S : MyMonadicSMemory) = struct
     in
     let pp_one ft (loc, fv_pairs) = pf ft "@[%s |-> %a@]" loc S.pp fv_pairs in
     (list ~sep:(any "@\n") pp_one) ft sorted_locs_with_vals
+
+  let get_recovery_tactic s e =
+    let current_recovery =
+      (* We use the regular recovery tactic of the map *)
+      get_recovery_tactic s e
+    in
+    match current_recovery.try_unfold with
+    | Some l ->
+        let alocs =
+          List.filter
+            (function
+              | Expr.ALoc _ | Lit (Loc _) -> true
+              | _ -> false)
+            l
+        in
+        if List.is_empty alocs then
+          (* Saves us some iterations *)
+          current_recovery
+        else
+          let locs_to_add =
+            States.MyUtils.SMap.fold
+              (fun key obj acc ->
+                match S.get_metadata obj with
+                | Some e when List.exists (Expr.equal e) alocs -> key :: acc
+                | _ -> acc)
+              s []
+          in
+          let expr_to_add = List.map Expr.loc_from_loc_name locs_to_add in
+          let try_unfold =
+            Some (List.sort_uniq Expr.compare (expr_to_add @ l))
+          in
+          { current_recovery with try_unfold }
+    | None -> current_recovery
 end
 
 (* When allocating, two params are given:
@@ -269,6 +335,7 @@ struct
         let ss, v = Obj.instantiate [ v ] in
         let s' = set ~idx ~idx':idx ss s in
         Delayed_result.ok (s', idx :: v)
+    | "alloc", _ -> failwith "Invalid arguments for alloc"
     | _ -> execute_action a s args
 end
 
diff --git a/transformers/lib/prebuilt/c_states/BlockTree.ml b/transformers/lib/prebuilt/c_states/BlockTree.ml
index 531dbc91..85ad66f9 100644
--- a/transformers/lib/prebuilt/c_states/BlockTree.ml
+++ b/transformers/lib/prebuilt/c_states/BlockTree.ml
@@ -1655,7 +1655,7 @@ module M = struct
     let svarr_subst = SVal.SVArray.subst ~le_subst in
     substitution ~le_subst ~sval_subst ~svarr_subst s |> Delayed.return
 
-  let get_recovery_tactic _ = Gillian.General.Recovery_tactic.none
+  let get_recovery_tactic _ _ = Gillian.General.Recovery_tactic.none
 
   let instantiate = function
     | [ low; high ] ->
diff --git a/transformers/lib/prebuilt/c_states/CGEnv.ml b/transformers/lib/prebuilt/c_states/CGEnv.ml
index 44d53350..c1e7c045 100644
--- a/transformers/lib/prebuilt/c_states/CGEnv.ml
+++ b/transformers/lib/prebuilt/c_states/CGEnv.ml
@@ -56,7 +56,7 @@ module M : States.MyMonadicSMemory.S with type t = Global_env.t = struct
   let lvars _ = Gillian.Utils.Containers.SS.empty
   let alocs _ = Gillian.Utils.Containers.SS.empty
   let substitution_in_place _ s = Delayed.return s
-  let get_recovery_tactic _ = Gillian.General.Recovery_tactic.none
+  let get_recovery_tactic _ _ = Gillian.General.Recovery_tactic.none
   let list_actions () = [ (GetDef, [], []) ]
   let list_preds () = []
 end
diff --git a/transformers/lib/states/ActionAdder.ml b/transformers/lib/states/ActionAdder.ml
index 91235673..0dc171a0 100644
--- a/transformers/lib/states/ActionAdder.ml
+++ b/transformers/lib/states/ActionAdder.ml
@@ -15,7 +15,9 @@ module type ActionAddition = sig
 
   val can_fix : err_t -> bool
   val get_fixes : err_t -> string MyAsrt.t list list
-  val get_recovery_tactic : err_t -> Expr.t Gillian.General.Recovery_tactic.t
+
+  val get_recovery_tactic :
+    t -> err_t -> Expr.t Gillian.General.Recovery_tactic.t
 end
 
 module Make (A : ActionAddition) (S : MyMonadicSMemory.S with type t = A.t) =
@@ -69,7 +71,7 @@ struct
            @@ MyAsrt.map_cp (fun (p, i, o) ->
                   (S.pred_from_str p |> Option.get, i, o))
 
-  let get_recovery_tactic = function
-    | BaseErr e -> S.get_recovery_tactic e
-    | AddedErr e -> A.get_recovery_tactic e
+  let get_recovery_tactic s = function
+    | BaseErr e -> S.get_recovery_tactic s e
+    | AddedErr e -> A.get_recovery_tactic s e
 end
diff --git a/transformers/lib/states/Agreement.ml b/transformers/lib/states/Agreement.ml
index 68233b48..f7557d72 100644
--- a/transformers/lib/states/Agreement.ml
+++ b/transformers/lib/states/Agreement.ml
@@ -94,7 +94,7 @@ let assertions = function
 
 let assertions_others _ = []
 
-let get_recovery_tactic (e : err_t) : Values.t Recovery_tactic.t =
+let get_recovery_tactic _ (e : err_t) : Values.t Recovery_tactic.t =
   match e with
   (* | MissingState -> Recovery_tactic.try_unfold ??? *)
   | _ -> Recovery_tactic.none
diff --git a/transformers/lib/states/Exclusive.ml b/transformers/lib/states/Exclusive.ml
index 8bd28fff..92e17144 100644
--- a/transformers/lib/states/Exclusive.ml
+++ b/transformers/lib/states/Exclusive.ml
@@ -91,7 +91,7 @@ let assertions = function
   | Some v -> [ (Ex, [], [ v ]) ]
 
 let assertions_others _ = []
-let get_recovery_tactic _ = Recovery_tactic.none
+let get_recovery_tactic _ _ = Recovery_tactic.none
 let can_fix MissingState = true
 
 let get_fixes MissingState =
diff --git a/transformers/lib/states/Fractional.ml b/transformers/lib/states/Fractional.ml
index db0a02ae..bdc9c92e 100644
--- a/transformers/lib/states/Fractional.ml
+++ b/transformers/lib/states/Fractional.ml
@@ -111,7 +111,7 @@ let assertions = function
   | Some (v, q) -> [ (Frac, [ q ], [ v ]) ]
 
 let assertions_others _ = []
-let get_recovery_tactic _ = Recovery_tactic.none
+let get_recovery_tactic _ _ = Recovery_tactic.none
 
 let can_fix = function
   | _ -> false
diff --git a/transformers/lib/states/Freeable.ml b/transformers/lib/states/Freeable.ml
index f6027b42..7db77075 100644
--- a/transformers/lib/states/Freeable.ml
+++ b/transformers/lib/states/Freeable.ml
@@ -165,8 +165,9 @@ module Make (S : MyMonadicSMemory.S) :
     | SubState s -> S.assertions_others s
     | _ -> []
 
-  let get_recovery_tactic = function
-    | SubError e -> S.get_recovery_tactic e
+  let get_recovery_tactic s e =
+    match (s, e) with
+    | SubState s, SubError e -> S.get_recovery_tactic s e
     | _ -> Gillian.General.Recovery_tactic.none (* TODO *)
 
   let can_fix = function
diff --git a/transformers/lib/states/MList.ml b/transformers/lib/states/MList.ml
index d585ec23..db00615f 100644
--- a/transformers/lib/states/MList.ml
+++ b/transformers/lib/states/MList.ml
@@ -215,11 +215,16 @@ module Make (S : MyMonadicSMemory.S) :
   let assertions_others (b, _) =
     List.concat_map (fun (_, v) -> S.assertions_others v) (ExpMap.bindings b)
 
-  let get_recovery_tactic = function
+  let get_recovery_tactic (st : t) = function
     | SubError (idx, e) ->
+        let sub_recover =
+          match ExpMap.find_opt idx (fst st) with
+          | Some codom -> S.get_recovery_tactic codom e
+          | None -> Gillian.General.Recovery_tactic.none
+        in
         Gillian.General.Recovery_tactic.merge
           (Gillian.General.Recovery_tactic.try_unfold [ idx ])
-          (S.get_recovery_tactic e)
+          sub_recover
     | _ -> Gillian.General.Recovery_tactic.none
 
   let can_fix = function
diff --git a/transformers/lib/states/MyMonadicSMemory.ml b/transformers/lib/states/MyMonadicSMemory.ml
index a4e48b0f..fb5fbf5d 100644
--- a/transformers/lib/states/MyMonadicSMemory.ml
+++ b/transformers/lib/states/MyMonadicSMemory.ml
@@ -70,7 +70,7 @@ module type S = sig
 
   (** The recovery tactic to attempt to resolve an error, by eg. unfolding
       predicates *)
-  val get_recovery_tactic : err_t -> Expr.t Recovery_tactic.t
+  val get_recovery_tactic : t -> err_t -> Expr.t Recovery_tactic.t
 
   (** The set of logical variables in the state *)
   val lvars : t -> Containers.SS.t
@@ -186,6 +186,5 @@ struct
   (* Override methods to keep implementations light *)
   let clear _ = empty ()
   let pp_err = pp_err_t
-  let get_recovery_tactic _ = get_recovery_tactic
   let pp_by_need _ = pp
 end
diff --git a/transformers/lib/states/PMap.ml b/transformers/lib/states/PMap.ml
index 4a450a46..e6c7137e 100644
--- a/transformers/lib/states/PMap.ml
+++ b/transformers/lib/states/PMap.ml
@@ -45,6 +45,7 @@ module type PMapImpl = sig
   type entry
   type t [@@deriving yojson]
 
+  val find_opt_unsafe : t -> Expr.t -> entry option
   val mode : index_mode
 
   (** Creates a new address, for allocating new state. Only used in static mode
@@ -98,7 +99,7 @@ end
 module type PMapType = sig
   include OpenPMapType
 
-  val domain_add : Expr.t -> t -> t
+  val domain_add : Expr.t -> t -> t Delayed.t
 end
 
 module Make
@@ -174,14 +175,12 @@ struct
 
   let domain_add k ((h, d) : t) =
     match d with
-    | None -> (h, d)
-    | Some (Expr.ESet d) -> (h, Some (Expr.ESet (k :: d)))
-    | Some _ ->
-        (* Currently we only support "concrete" domain sets (ie. using Expr.ESet, instead of
-           as logical variables). To add support to "symbolic" domain sets one would need
-           to make this function return a Expr.t Delayed.t, adding to the PC that the key is in
-           the set. *)
-        failwith "Invalid index set; expected a set"
+    | None -> Delayed.return (h, d)
+    | Some (Expr.ESet d) -> Delayed.return (h, Some (Expr.ESet (k :: d)))
+    | Some d ->
+        let open Delayed.Syntax in
+        let+ d' = Delayed.reduce (NOp (SetUnion, [ d; ESet [ k ] ])) in
+        (h, Some d')
 
   let get ((h, d) as s) idx =
     let open Delayed.Syntax in
@@ -204,7 +203,7 @@ struct
               | Dynamic ->
                   let ss, _ = S.instantiate I.default_instantiation in
                   let h' = I.set ~idx:idx' ~idx':idx ss h in
-                  let s' = (h', Some d) |> domain_add idx' in
+                  let* s' = domain_add idx' (h', Some d) in
                   DR.ok (s', idx', ss)))
 
   let set ~idx ~idx' entry ((h, d) : t) = (I.set ~idx ~idx' entry h, d)
@@ -234,7 +233,8 @@ struct
           failwith "Alloc not allowed using dynamic indexing";
         let* idx = I.make_fresh () in
         let ss, v = S.instantiate args in
-        let s' = set ~idx ~idx':idx ss s |> domain_add idx in
+        let s' = set ~idx ~idx':idx ss s in
+        let* s' = domain_add idx s' in
         DR.ok (s', idx :: v)
     | GetDomainSet, [] -> (
         match s with
@@ -373,9 +373,14 @@ struct
   let assertions_others (h, _) =
     I.fold (fun _ s acc -> S.assertions_others s @ acc) h []
 
-  let get_recovery_tactic = function
+  let get_recovery_tactic (st : t) = function
     | SubError (_, idx, e) ->
-        Gillian.General.Recovery_tactic.merge (S.get_recovery_tactic e)
+        let sub_recover =
+          match I.find_opt_unsafe (fst st) idx with
+          | Some codom -> S.get_recovery_tactic codom e
+          | None -> Gillian.General.Recovery_tactic.none
+        in
+        Gillian.General.Recovery_tactic.merge sub_recover
           (Gillian.General.Recovery_tactic.try_unfold [ idx ])
     | NotAllocated idx | InvalidIndexValue idx ->
         Gillian.General.Recovery_tactic.try_unfold [ idx ]
@@ -540,9 +545,14 @@ struct
   let assertions_others h =
     I.fold (fun _ s acc -> S.assertions_others s @ acc) h []
 
-  let get_recovery_tactic = function
+  let get_recovery_tactic (st : t) = function
     | SubError (_, idx, e) ->
-        Gillian.General.Recovery_tactic.merge (S.get_recovery_tactic e)
+        let sub_recover =
+          match I.find_opt_unsafe st idx with
+          | Some codom -> S.get_recovery_tactic codom e
+          | None -> Gillian.General.Recovery_tactic.none
+        in
+        Gillian.General.Recovery_tactic.merge sub_recover
           (Gillian.General.Recovery_tactic.try_unfold [ idx ])
     | InvalidIndexValue idx ->
         Gillian.General.Recovery_tactic.try_unfold [ idx ]
@@ -642,6 +652,7 @@ struct
   type entry = S.t
   type t = S.t ExpMap.t [@@deriving yojson]
 
+  let find_opt_unsafe h idx = ExpMap.find_opt idx h
   let mode = I.mode
   let make_fresh = I.make_fresh
   let default_instantiation = I.default_instantiation
@@ -681,6 +692,11 @@ struct
   type entry = S.t
   type t = S.t ExpMap.t * S.t ExpMap.t [@@deriving yojson]
 
+  let find_opt_unsafe (h1, h2) idx =
+    match ExpMap.find_opt idx h1 with
+    | Some v -> Some v
+    | None -> ExpMap.find_opt idx h2
+
   let mode = I.mode
   let make_fresh = I.make_fresh
   let default_instantiation = I.default_instantiation
@@ -755,7 +771,17 @@ module ALocImpl (S : MyMonadicSMemory.S) = struct
   module SMap = MyUtils.SMap
 
   type entry = S.t
-  type t = S.t MyUtils.SMap.t [@@deriving yojson]
+  type t = S.t SMap.t [@@deriving yojson]
+
+  let find_opt_unsafe h idx =
+    let open Utils.Syntaxes.Option in
+    let* loc =
+      match idx with
+      | Expr.Lit (Loc loc) -> Some loc
+      | Expr.ALoc loc -> Some loc
+      | _ -> None
+    in
+    SMap.find_opt loc h
 
   let mode : index_mode = Static
   let make_fresh () = ALoc.alloc () |> Expr.loc_from_loc_name |> Delayed.return
diff --git a/transformers/lib/states/PMap.mli b/transformers/lib/states/PMap.mli
index fa7ee0c9..ffad22cb 100644
--- a/transformers/lib/states/PMap.mli
+++ b/transformers/lib/states/PMap.mli
@@ -7,6 +7,7 @@ module type PMapImpl = sig
   type entry
   type t [@@deriving yojson]
 
+  val find_opt_unsafe : t -> Expr.t -> entry option
   val mode : index_mode
   val make_fresh : unit -> Expr.t Delayed.t
   val default_instantiation : Expr.t list
@@ -32,7 +33,7 @@ end
 module type PMapType = sig
   include OpenPMapType
 
-  val domain_add : Expr.t -> t -> t
+  val domain_add : Expr.t -> t -> t Delayed.t
 end
 
 module Make
diff --git a/transformers/lib/states/Product.ml b/transformers/lib/states/Product.ml
index eca0bf7a..57a74840 100644
--- a/transformers/lib/states/Product.ml
+++ b/transformers/lib/states/Product.ml
@@ -124,9 +124,9 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) :
   let assertions_others (s1, s2) =
     S1.assertions_others s1 @ S2.assertions_others s2
 
-  let get_recovery_tactic = function
-    | E1 e -> S1.get_recovery_tactic e
-    | E2 e -> S2.get_recovery_tactic e
+  let get_recovery_tactic (s1, s2) = function
+    | E1 e -> S1.get_recovery_tactic s1 e
+    | E2 e -> S2.get_recovery_tactic s2 e
 
   let can_fix = function
     | E1 e -> S1.can_fix e
diff --git a/transformers/lib/states/Sum.ml b/transformers/lib/states/Sum.ml
index c0ce1112..889b8a6b 100644
--- a/transformers/lib/states/Sum.ml
+++ b/transformers/lib/states/Sum.ml
@@ -179,10 +179,10 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) :
     | S2 s2 -> S2.assertions_others s2
     | None -> []
 
-  let get_recovery_tactic e =
-    match e with
-    | E1 e1 -> S1.get_recovery_tactic e1
-    | E2 e2 -> S2.get_recovery_tactic e2
+  let get_recovery_tactic st e =
+    match (st, e) with
+    | S1 s1, E1 e1 -> S1.get_recovery_tactic s1 e1
+    | S2 s2, E2 e2 -> S2.get_recovery_tactic s2 e2
     | _ -> failwith "get_recovery_tactic: mismatched arguments"
 
   let can_fix = function