mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
.NET and Java API Bugfix (Codeplex issue 101)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
7bb1469d71
commit
944dfee008
|
@ -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));
|
||||
}
|
||||
|
|
|
@ -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)));
|
||||
|
|
Loading…
Reference in a new issue