Do additional simplifications to history thread ID may_create

src/cdomain/value/cdomains/threadIdDomain.ml

@@ -156,10 +156,10 @@ struct
     else if is_unique t then ( (* t' is already non-unique *)
       let cdef_ancestor = P.common_suffix p p' in
       if P.equal cdef_ancestor p then ( (* p is prefix of p' *)
-        (* TODO: avoid length calculations? *)
-        let dp = BatList.take (List.length p' - List.length cdef_ancestor) p' in (* elements added to prefix *)
-        S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *)
-        (* TODO: no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway? *)
+        (* let dp = elements added to prefix *)
+        (* S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *) *)
+        (* no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway *)
+        true
       )
       else if P.equal cdef_ancestor p' then ( (* p is not prefix of p', but p' is prefix of p *)
         (* TODO: avoid length calculations? *)
@@ -172,9 +172,15 @@ struct
     )
     else ( (* both are non-unique *)
       let cdef_ancestor = P.common_suffix p p' in
-      P.equal cdef_ancestor p' && (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
-      S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
-      (* TODO: can just subset s' thanks to well-formedness conditions? *)
+      if P.equal cdef_ancestor p' then ( (* p' is prefix of p *)
+        (* TODO: avoid length calculations? *)
+        let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *)
+        S.subset (S.union (S.of_list dp') s) s' (* elements must be contained, because compose can only add them *)
+        (* can just subset s' thanks to well-formedness conditions *)
+        (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *)
+      )
+      else
+        false (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
     )
 
   let compose ((p, s) as current) ni =

tests/unit/cdomains/threadIdDomainTest.ml

@@ -93,6 +93,8 @@ let test_history_may_create _ =
   assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> a));
   assert_equal true (may_create (main >> a >> b >> b) (main >> b >> b >> a));
   assert_equal true (may_create (main >> a >> b >> b) (main >> b >> a >> b));
+
+  (* 4f6a7637b8d0dc723fe382f94bed6c822cd4a2ce passes all... *)
   ()
 
 let tests =