From ee22d4054201afd40c9a7bf05fe9fb8ca808639f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Apr 2014 19:18:43 +0100 Subject: [PATCH] ML API bugfix Signed-off-by: Christoph M. Wintersteiger --- src/api/ml/z3.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index d91d3ca8d..5f8d96d2a 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -793,7 +793,7 @@ end = struct mk_list f n let update ( x : expr ) ( args : expr list ) = - if (List.length args <> (get_num_args x)) then + if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then raise (Z3native.Exception "Number of arguments does not match") else expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args))