diff --git a/compiler/verification/.z3backend.real.ml.swp b/compiler/verification/.z3backend.real.ml.swp deleted file mode 100644 index b079121a..00000000 Binary files a/compiler/verification/.z3backend.real.ml.swp and /dev/null differ diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 27a512a2..6b414df0 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -742,7 +742,6 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = | EArray _ -> failwith "[Z3 encoding] EArray unsupported" | ELit l -> ctx, translate_lit ctx l | EAbs _ -> failwith "[Z3 encoding] EAbs unsupported" - | EApp { f = head; args = [] } -> failwith "[Z3 encoding] let in" | EApp { f = head; args } -> ( match Marked.unmark head with | EOp { op; _ } -> translate_op ctx op args