From f342c8948202930370bc976bd13cc89be056226a Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 12 Jan 2022 19:15:51 +0100
Subject: [PATCH] [skip ci] Z3encoding: proper error message for ill-formed
 unary operators

---
 compiler/verification/z3encoding.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/compiler/verification/z3encoding.ml b/compiler/verification/z3encoding.ml
index 8145aaf0..bf044196 100644
--- a/compiler/verification/z3encoding.ml
+++ b/compiler/verification/z3encoding.ml
@@ -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