From 1cc38814b93e31e624ecf95b2a3fb42ee76f4608 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 7 Jan 2025 09:16:50 +0000 Subject: [PATCH] Report locations for missing SMT generators --- src/sail_smt_backend/jib_smt.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index bcad6b137..6f7f04aa4 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -553,7 +553,7 @@ module Make (Config : CONFIG) = struct | Some generator -> let* value = generator args ret_ctyp in singleton (define_const id ret_ctyp value) - | None -> failwith ("No generator " ^ string_of_id function_id) + | None -> raise (Reporting.err_general l ("No generator " ^ string_of_id function_id)) ) ) else if extern && string_of_id function_id = "internal_vector_init" then singleton (declare_const id ret_ctyp)