Normalisation through assert_norm crashes F*

[R1kM]

The following code crashes when using F* master, commit 95984a8067e8be3e2.

let sprop = bool -> prop

let pred (args: list bool) : sprop =
  let rec aux (args:list bool) (out:sprop) : sprop =
  match args with
  | [] -> out
  | a::q -> let out:sprop = fun s0 -> out s0 in aux q out
  in aux args (fun _ -> True)

let lemma_pred (args:list bool) : Lemma (pred args true) =
  match args with
  | [] -> assert_norm (pred args true)
  | _ -> admit()

In interactive mode, typechecking lemma_pred yields [F error] FStar_SMTEncoding_Env.Inner_let_rec F: subprocess exited.

Replacing assert_norm (pred args true) by assert_norm (pred [] true) solves the issue. Nevertheless, this should probably be a warning instead of a crash

[aseemr]

F* now gives a warning (at the definition of aux) and an error (in lemma_pred) as follows:

(Warning) Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types
(Error) Could not encode the query since F* does not support precise smtencoding of inner let-recs yet (in this case aux)

Closing the issue, thanks for the report!