From 944dfee008a63673184008b7bb334cf0b7c04331 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 2 Apr 2014 19:25:05 +0100 Subject: [PATCH] .NET and Java API Bugfix (Codeplex issue 101) Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Expr.cs | 2 +- src/api/java/Expr.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index dae4df445..c8fdfb51f 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -99,7 +99,7 @@ namespace Microsoft.Z3 Contract.Requires(Contract.ForAll(args, a => a != null)); Context.CheckContextMatch(args); - if (args.Length != NumArgs) + if (IsApp && args.Length != NumArgs) throw new Z3Exception("Number of arguments does not match"); NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args)); } diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 5c4f90920..f7edc6a2b 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -94,7 +94,7 @@ public class Expr extends AST public void update(Expr[] args) throws Z3Exception { getContext().checkContextMatch(args); - if (args.length != getNumArgs()) + if (isApp() && args.length != getNumArgs()) throw new Z3Exception("Number of arguments does not match"); setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(), (int) args.length, Expr.arrayToNative(args)));