From 4e1068142fc6ded14dc8d67272b0fb39d79d6996 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 13 Oct 2018 17:59:10 -0500 Subject: [PATCH] fix(model): add a constant to unin types with empty domains close #5 --- src/Solver.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Solver.ml b/src/Solver.ml index ee08ded..229bd6d 100644 --- a/src/Solver.ml +++ b/src/Solver.ml @@ -3691,7 +3691,12 @@ module Make(Config : CONFIG)(Dummy : sig end) = struct let domains = Ty.Tbl.to_seq doms |> Sequence.map - (fun (ty,dom) -> Conv.ty_to_ast ty, List.map Typed_cst.id dom) + (fun (ty,dom) -> + let dom = match dom with + | [] -> [ID.make (Printf.sprintf "$%s_0" (Ty.mangle ty))] + | l -> List.map Typed_cst.id l + in + Conv.ty_to_ast ty, dom) |> Ast.Ty.Map.of_seq in Model.make ~env ~consts ~domains