CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 16:28:12 +03:00
Code Issues Projects Releases Wiki Activity

[skip ci] Z3encoding: proper error message for ill-formed unary operators

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-01-12 19:15:51 +01:00
parent d6205369bb
commit f342c89482
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
compiler/verification/z3encoding.ml
View File

@ -198,8 +198,11 @@ let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked lis
let ctx, e1 =
match args with
| [ e1 ] -> translate_expr ctx e1
(* TODO: Print term for error message *)
| _ -> failwith "[Z3 encoding] Ill-formed unary operator application"
| _ ->
failwith
(Format.asprintf "[Z3 encoding] Ill-formed unary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
in
match uop with