lemma bounded_nth xs ls us n =
match (List.nth n xs), (List.nth n ls), (List.nth n us) with
| Some x, Some l, Some u -> l <=. x && x <=. u
| _, _, _ -> true
[@@by auto]
(note that the proof of the lemma is supposed to fail)
Error message:
Validation failed:
(Invalid_model (
Error{ Kind.name = "ValidationError" }:
Model validation failed because of free variables in the goal:
(ls/30984 : real list), (n/30992 : int), (us/30988 : real list),
(xs/30980 : real list). This is a bug in ImandraX.
backtrace:
Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 395, characters 21-36
Called from Imandrax_lower_rir__Rir_to_cir.to_term_rec_ in file "src/lower-rir/rir_to_cir.ml", line 208, characters 8-32,
{ tys = []; consts = []; funs = []; representable = true;
completed = true; ty_subst = [] }
))
[task](http://localhost:37829/po-task/by-name/%2Fhome%2Fremi%2Fsource%2Fimandra-marabou-proof-checking%2Fimandrax%2Ferror_test.iml/bounded_nth/by-id/task%3Apo%3AK0_eJJwMG7u78-nhp-oOSVI-8kFCEFJYk2IEbmEClM4%3D)lsp
Code:
(note that the proof of the lemma is supposed to fail) Error message: