From ea9c4452b2eb8aa255af911ef3cc1088fb80b1f8 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 26 Apr 2018 16:57:52 +0100
Subject: Lem: Add Size class annotations for nested bitvector types

---
 src/pretty_print_lem.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 15cd0512..f58c3fa6 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -439,7 +439,13 @@ let rec typeclass_nexps (Typ_aux(t,_)) =
        let size_nexp = nexp_simp size_nexp in
        if is_nexp_constant size_nexp then NexpSet.empty else
        NexpSet.singleton (orig_nexp size_nexp)
-    | Typ_app _ -> NexpSet.empty
+    | Typ_app (id, args) ->
+       let add_arg_nexps nexps = function
+         | Typ_arg_aux (Typ_arg_typ typ, _) ->
+            NexpSet.union nexps (typeclass_nexps typ)
+         | _ -> nexps
+       in
+       List.fold_left add_arg_nexps NexpSet.empty args
     | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *)
   else NexpSet.empty
 
-- 
cgit v1.2.3