fix(model): add a constant to unin types with empty domains

close #5
c-cube · Oct 13, 2018 · 4e10681 · 4e10681
1 parent a4deb1c
commit 4e10681
Showing 1 changed file with 6 additions and 1 deletion.
diff --git 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