Skip to content

Commit

Permalink
Improve error message.
Browse files Browse the repository at this point in the history
  • Loading branch information
gebner committed Jan 3, 2025
1 parent b20569e commit b734fe4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/smtencoding/FStarC.SMTEncoding.Env.fst
Original file line number Diff line number Diff line change
Expand Up @@ -301,7 +301,7 @@ let push_zfuel_name env (x:lident) f ftok =
{env with fvar_bindings=add_fvar_binding fvb env.fvar_bindings}
let force_thunk fvb =
if not (fvb.fvb_thunked) || fvb.smt_arity <> 0
then failwith "Forcing a non-thunk in the SMT encoding";
then failwith (BU.format1 "Forcing a non-thunk %s in the SMT encoding" (string_of_lid fvb.fvar_lid));
mkFreeV <| FV (fvb.smt_id, Term_sort, true)
module TcEnv = FStarC.TypeChecker.Env
let try_lookup_free_var env l =
Expand Down

0 comments on commit b734fe4

Please sign in to comment.