diff --git a/_feat_ b/_feat_
diff --git a/_lazysc_ b/_lazysc_
diff --git a/bench-log-mon-night b/bench-log-mon-night
diff --git a/bench-log-tue-night b/bench-log-tue-night
diff --git a/bench-wed-cvc4 b/bench-wed-cvc4
diff --git a/benchmarks/grammars/packrat_unambigPackrat.smt2 b/benchmarks/grammars/packrat_unambigPackrat.smt2
@@ -2,9 +2,9 @@
 (declare-datatypes (a)
   ((list (nil) (cons (head a) (tail (list a))))))
 (declare-datatypes () ((Tok (X) (Y) (Z))))
-(declare-datatypes () ((B2 (SB (SB_0 B2)) (ZB))))
-(declare-datatypes () ((A2 (SA (SA_0 A2)) (ZA))))
-(declare-datatypes () ((S (A (A_0 A2)) (B (B_0 B2)))))
+(declare-datatypes () ((B (SB (SB_0 B)) (ZB))))
+(declare-datatypes () ((A (SA (SA_0 A)) (ZA))))
+(declare-datatypes () ((S (A2 (A_0 A)) (B2 (B_0 B)))))
 (define-fun-rec
   (par (a)
     (append
@@ -14,15 +14,15 @@
          (case (cons z xs) (cons z (append xs y)))))))
 (define-fun-rec
   linA
-    ((x A2)) (list Tok)
+    ((x A)) (list Tok)
     (match x
       (case (SA a)
         (append (append (cons X (as nil (list Tok))) (linA a))
           (cons Y (as nil (list Tok)))))
       (case ZA (cons X (cons Z (cons Y (as nil (list Tok))))))))
 (define-fun-rec
   linB
-    ((x B2)) (list Tok)
+    ((x B)) (list Tok)
     (match x
       (case (SB b)
         (append (append (cons X (as nil (list Tok))) (linB b))
@@ -32,8 +32,8 @@
   linS
     ((x S)) (list Tok)
     (match x
-      (case (A a) (linA a))
-      (case (B b) (linB b))))
+      (case (A2 a) (linA a))
+      (case (B2 b) (linB b))))
 (assert-not
   (forall ((u S) (v S)) (=> (= (linS u) (linS v)) (= u v))))
 (check-sat)
diff --git a/benchmarks/isaplanner/prop_85.smt2 b/benchmarks/isaplanner/prop_85.smt2
@@ -17,6 +17,13 @@
            (match y
              (case nil (as nil (list (Pair a b))))
              (case (cons x3 x4) (cons (Pair2 z x3) (zip x2 x4)))))))))
+(define-fun-rec
+  (par (a)
+    (len
+       ((x (list a))) Nat
+       (match x
+         (case nil Z)
+         (case (cons y xs) (S (len xs)))))))
 (define-fun-rec
   (par (a)
     (append
@@ -33,5 +40,6 @@
          (case (cons y xs) (append (rev xs) (cons y (as nil (list a)))))))))
 (assert-not
   (forall ((xs (list Nat)) (ys (list Nat)))
-    (= (zip (rev xs) (rev ys)) (rev (zip xs ys)))))
+    (=> (= (len xs) (len ys))
+      (= (zip (rev xs) (rev ys)) (rev (zip xs ys))))))
 (check-sat)
diff --git a/benchmarks/sat/bsort_inj_len_both_n02.smt2 b/benchmarks/sat/bsort_inj_len_both_n02.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n03.smt2 b/benchmarks/sat/bsort_inj_len_both_n03.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n04.smt2 b/benchmarks/sat/bsort_inj_len_both_n04.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n05.smt2 b/benchmarks/sat/bsort_inj_len_both_n05.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n06.smt2 b/benchmarks/sat/bsort_inj_len_both_n06.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n07.smt2 b/benchmarks/sat/bsort_inj_len_both_n07.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n08.smt2 b/benchmarks/sat/bsort_inj_len_both_n08.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n09.smt2 b/benchmarks/sat/bsort_inj_len_both_n09.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n10.smt2 b/benchmarks/sat/bsort_inj_len_both_n10.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n11.smt2 b/benchmarks/sat/bsort_inj_len_both_n11.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n12.smt2 b/benchmarks/sat/bsort_inj_len_both_n12.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n13.smt2 b/benchmarks/sat/bsort_inj_len_both_n13.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n14.smt2 b/benchmarks/sat/bsort_inj_len_both_n14.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n15.smt2 b/benchmarks/sat/bsort_inj_len_both_n15.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n16.smt2 b/benchmarks/sat/bsort_inj_len_both_n16.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n17.smt2 b/benchmarks/sat/bsort_inj_len_both_n17.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n18.smt2 b/benchmarks/sat/bsort_inj_len_both_n18.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n19.smt2 b/benchmarks/sat/bsort_inj_len_both_n19.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n20.smt2 b/benchmarks/sat/bsort_inj_len_both_n20.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n21.smt2 b/benchmarks/sat/bsort_inj_len_both_n21.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n22.smt2 b/benchmarks/sat/bsort_inj_len_both_n22.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n23.smt2 b/benchmarks/sat/bsort_inj_len_both_n23.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n24.smt2 b/benchmarks/sat/bsort_inj_len_both_n24.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n25.smt2 b/benchmarks/sat/bsort_inj_len_both_n25.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n26.smt2 b/benchmarks/sat/bsort_inj_len_both_n26.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n27.smt2 b/benchmarks/sat/bsort_inj_len_both_n27.smt2
diff --git a/benchmarks/sat/bsort_inj_len_both_n28.smt2 b/benchmarks/sat/bsort_inj_len_both_n28.smt2