mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

ML API bugfix

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-04-02 19:18:43 +01:00
parent 54b7f8eec3
commit ee22d40542
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/ml/z3.ml
View file

@ -793,7 +793,7 @@ end = struct
mk_list f n mk_list f n
let update ( x : expr ) ( args : expr list ) = 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") raise (Z3native.Exception "Number of arguments does not match")
else else
expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args))